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 SNo : set prop const Empty : set axiom SNo_0: SNo Empty const ordsucc : set set axiom SNo_2: SNo (ordsucc (ordsucc Empty)) const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoLt_0_2: Empty < ordsucc (ordsucc Empty) const nat_p : set prop const exp_SNo_nat : set set set axiom exp_SNo_nat_pos: !x:set.SNo x -> Empty < x -> !y:set.nat_p y -> Empty < exp_SNo_nat x y const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom add_SNo_0R: !x:set.SNo x -> x + Empty = x const Sep : set (set prop) set const SNoS_ : set set const omega : set const SNoLev : set set const ordinal : set prop lemma !x:set.nat_p x -> equip (Sep (SNoS_ omega) \y:set.SNoLev y = x) (exp_SNo_nat (ordsucc (ordsucc Empty)) 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 -> equip (Sep (SNoS_ omega) \y:set.SNoLev y = ordsucc x) (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x) var x:set hyp nat_p x hyp equip (Sep (SNoS_ omega) \y:set.SNoLev y = x) (exp_SNo_nat (ordsucc (ordsucc Empty)) 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) claim (!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) -> equip (Sep (SNoS_ omega) \y:set.SNoLev y = ordsucc x) (exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x)