const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term TransSet = \x:set.!y:set.y iIn x -> Subq y x term ordinal = \x:set.TransSet x & !y:set.y iIn x -> TransSet y term nIn = \x:set.\y:set.~ x iIn y const SNo : set prop const minus_SNo : set set term - = minus_SNo axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x const SNoLev : set set axiom SNoLev_ordinal: !x:set.SNo x -> ordinal (SNoLev x) const ordsucc : set set axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) const SNoR : set set const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoR_E: !x:set.SNo x -> !y:set.y iIn SNoR x -> !P:prop.(SNo y -> SNoLev y iIn SNoLev x -> x < y -> P) -> P const Repl : set (set set) set axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P const famunion : set (set set) set axiom ordinal_famunion: !x:set.!f:set set.(!y:set.y iIn x -> ordinal (f y)) -> ordinal (famunion x f) const SNoL : set set axiom SNoL_E: !x:set.SNo x -> !y:set.y iIn SNoL x -> !P:prop.(SNo y -> SNoLev y iIn SNoLev x -> y < x -> P) -> P const binunion : set set set axiom ordinal_binunion: !x:set.!y:set.ordinal x -> ordinal y -> ordinal (binunion x y) const SNoCutP : set set prop const SNoCut : set set set const SNoEq_ : set set set prop axiom SNoCutP_SNoCut_impred: !x:set.!y:set.SNoCutP x y -> !P:prop.(SNo (SNoCut x y) -> SNoLev (SNoCut x y) iIn ordsucc (binunion (famunion x \z:set.ordsucc (SNoLev z)) (famunion y \z:set.ordsucc (SNoLev z))) -> (!z:set.z iIn x -> z < SNoCut x y) -> (!z:set.z iIn y -> SNoCut x y < z) -> (!z:set.SNo z -> (!w:set.w iIn x -> w < z) -> (!w:set.w iIn y -> z < w) -> Subq (SNoLev (SNoCut x y)) (SNoLev z) & SNoEq_ (SNoLev (SNoCut x y)) (SNoCut x y) z) -> P) -> P axiom minus_SNo_eq: !x:set.SNo x -> - x = SNoCut (Repl (SNoR x) minus_SNo) (Repl (SNoL x) minus_SNo) const SNoS_ : set set lemma !x:set.!y:set.TransSet x -> (!z:set.z iIn x -> !w:set.w iIn SNoS_ z -> Subq (SNoLev - w) (SNoLev w)) -> SNoLev y iIn x -> ordinal (SNoLev y) -> SNo y -> SNoLev (SNoCut (Repl (SNoR y) minus_SNo) (Repl (SNoL y) minus_SNo)) iIn ordsucc (binunion (famunion (Repl (SNoR y) minus_SNo) \z:set.ordsucc (SNoLev z)) (famunion (Repl (SNoL y) minus_SNo) \z:set.ordsucc (SNoLev z))) -> ordinal (binunion (famunion (Repl (SNoR y) minus_SNo) \z:set.ordsucc (SNoLev z)) (famunion (Repl (SNoL y) minus_SNo) \z:set.ordsucc (SNoLev z))) -> !z:set.z iIn SNoLev (SNoCut (Repl (SNoR y) minus_SNo) (Repl (SNoL y) minus_SNo)) -> z iIn SNoLev y var x:set var y:set hyp TransSet x hyp !z:set.z iIn x -> !w:set.w iIn SNoS_ z -> Subq (SNoLev - w) (SNoLev w) hyp SNoLev y iIn x hyp ordinal (SNoLev y) hyp SNo y claim SNoCutP (Repl (SNoR y) minus_SNo) (Repl (SNoL y) minus_SNo) -> Subq (SNoLev - y) (SNoLev y)