const bij : set set (set set) prop term equip = \x:set.\y:set.?f:set set.bij x y f const In : set set prop term iIn = In infix iIn 2000 2000 term PNoEq_ = \x:set.\p:set prop.\q:set prop.!y:set.y iIn x -> (p y <-> q y) term nIn = \x:set.\y:set.~ x iIn y term SNoEq_ = \x:set.\y:set.\z:set.PNoEq_ x (\w:set.w iIn y) \w:set.w iIn z const If_i : prop set set set axiom If_i_1: !P:prop.!x:set.!y:set.P -> If_i P x y = x axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y const nat_p : set prop const exp_SNo_nat : set set set const ordsucc : set set const Empty : set const ordinal : set prop const SNo : set prop const add_SNo : set set set term + = add_SNo infix + 2281 2280 const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const Sep : set (set prop) set const SNoS_ : set set const omega : set const SNoLev : set set const binintersect : set set set const SNoElts_ : set set lemma !x:set.!f:set set.nat_p x -> nat_p (exp_SNo_nat (ordsucc (ordsucc Empty)) x) -> ordinal (exp_SNo_nat (ordsucc (ordsucc Empty)) x) -> SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) x) -> nat_p (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x) -> ordinal (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x) -> SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x) -> (!y:set.SNo y -> y < exp_SNo_nat (ordsucc (ordsucc Empty)) x -> (exp_SNo_nat (ordsucc (ordsucc Empty)) x + y) < exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x) -> exp_SNo_nat (ordsucc (ordsucc Empty)) x < exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x -> (!y:set.y iIn Sep (SNoS_ omega) (\z:set.SNoLev z = x) -> !z:set.z iIn Sep (SNoS_ omega) (\w:set.SNoLev w = x) -> f y = f z -> y = z) -> (!y:set.y iIn exp_SNo_nat (ordsucc (ordsucc Empty)) x -> ?z:set.z iIn Sep (SNoS_ omega) (\w:set.SNoLev w = x) & f z = y) -> (!y:set.y iIn Sep (SNoS_ omega) (\z:set.SNoLev z = ordsucc x) -> !P:prop.(SNo y -> SNoLev y = ordsucc x -> binintersect y (SNoElts_ x) iIn Sep (SNoS_ omega) (\z:set.SNoLev z = x) -> SNo (binintersect y (SNoElts_ x)) -> SNoLev (binintersect y (SNoElts_ x)) = x -> P) -> P) -> (!y:set.y iIn Sep (SNoS_ omega) (\z:set.SNoLev z = ordsucc x) -> !P:prop.(nat_p (f (binintersect y (SNoElts_ x))) -> ordinal (f (binintersect y (SNoElts_ x))) -> SNo (f (binintersect y (SNoElts_ x))) -> f (binintersect y (SNoElts_ x)) < exp_SNo_nat (ordsucc (ordsucc Empty)) x -> P) -> P) -> (?f2:set set.(!y:set.x iIn y -> f2 y = f (binintersect y (SNoElts_ x))) & !y:set.nIn x y -> f2 y = exp_SNo_nat (ordsucc (ordsucc Empty)) x + f (binintersect y (SNoElts_ x))) -> ?f2:set set.bij (Sep (SNoS_ omega) \y:set.SNoLev y = ordsucc x) (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x) f2 var x:set var f:set set hyp nat_p x hyp nat_p (exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp ordinal (exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp nat_p (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp ordinal (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp !y:set.SNo y -> y < exp_SNo_nat (ordsucc (ordsucc Empty)) x -> (exp_SNo_nat (ordsucc (ordsucc Empty)) x + y) < exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x hyp exp_SNo_nat (ordsucc (ordsucc Empty)) x < exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x hyp !y:set.y iIn Sep (SNoS_ omega) (\z:set.SNoLev z = x) -> f y iIn exp_SNo_nat (ordsucc (ordsucc Empty)) x hyp !y:set.y iIn Sep (SNoS_ omega) (\z:set.SNoLev z = x) -> !z:set.z iIn Sep (SNoS_ omega) (\w:set.SNoLev w = x) -> f y = f z -> y = z hyp !y:set.y iIn exp_SNo_nat (ordsucc (ordsucc Empty)) x -> ?z:set.z iIn Sep (SNoS_ omega) (\w:set.SNoLev w = x) & f z = y hyp !y:set.y iIn Sep (SNoS_ omega) (\z:set.SNoLev z = ordsucc x) -> !P:prop.(SNo y -> SNoLev y = ordsucc x -> binintersect y (SNoElts_ x) iIn Sep (SNoS_ omega) (\z:set.SNoLev z = x) -> SNo (binintersect y (SNoElts_ x)) -> SNoLev (binintersect y (SNoElts_ x)) = x -> P) -> P claim (!y:set.y iIn Sep (SNoS_ omega) (\z:set.SNoLev z = ordsucc x) -> !P:prop.(nat_p (f (binintersect y (SNoElts_ x))) -> ordinal (f (binintersect y (SNoElts_ x))) -> SNo (f (binintersect y (SNoElts_ x))) -> f (binintersect y (SNoElts_ x)) < exp_SNo_nat (ordsucc (ordsucc Empty)) x -> P) -> P) -> equip (Sep (SNoS_ omega) \y:set.SNoLev y = ordsucc x) (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x)