const ordinal : set prop const SNo_ : set set prop term SNo = \x:set.?y:set.ordinal y & SNo_ y x const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const PNoLt : set (set prop) set (set prop) prop const SNoLev : set set term SNoLt = \x:set.\y:set.PNoLt (SNoLev x) (\z:set.z iIn x) (SNoLev y) \z:set.z iIn y term < = SNoLt infix < 2020 2020 const PNoEq_ : set (set prop) (set prop) prop term SNoEq_ = \x:set.\y:set.\z:set.PNoEq_ x (\w:set.w iIn y) \w:set.w iIn z axiom ordinal_Hered: !x:set.ordinal x -> !y:set.y iIn x -> ordinal y const binintersect : set set set axiom binintersectE: !x:set.!y:set.!z:set.z iIn binintersect x y -> z iIn x & z iIn y const PNoLt_ : set (set prop) (set prop) prop axiom PNoLt_E_: !x:set.!p:set prop.!q:set prop.PNoLt_ x p q -> !P:prop.(!y:set.y iIn x -> PNoEq_ y p q -> ~ p y -> q y -> P) -> P axiom PNoLtE: !x:set.!y:set.!p:set prop.!q:set prop.PNoLt x p y q -> !P:prop.(PNoLt_ (binintersect x y) p q -> P) -> (x iIn y -> PNoEq_ x p q -> q x -> P) -> (y iIn x -> PNoEq_ y p q -> ~ p y -> P) -> P lemma !x:set.!y:set.!P:prop.!z:set.(!w:set.SNo w -> SNoLev w iIn binintersect (SNoLev x) (SNoLev y) -> SNoEq_ (SNoLev w) w x -> SNoEq_ (SNoLev w) w y -> x < w -> w < y -> nIn (SNoLev w) x -> SNoLev w iIn y -> P) -> ordinal (SNoLev x) -> z iIn binintersect (SNoLev x) (SNoLev y) -> PNoEq_ z (\w:set.w iIn x) (\w:set.w iIn y) -> ~ z iIn x -> z iIn y -> z iIn SNoLev x -> z iIn SNoLev y -> ordinal z -> P var x:set var y:set var P:prop hyp SNo y hyp x < y hyp !z:set.SNo z -> SNoLev z iIn binintersect (SNoLev x) (SNoLev y) -> SNoEq_ (SNoLev z) z x -> SNoEq_ (SNoLev z) z y -> x < z -> z < y -> nIn (SNoLev z) x -> SNoLev z iIn y -> P hyp SNoLev x iIn SNoLev y -> SNoEq_ (SNoLev x) x y -> SNoLev x iIn y -> P hyp SNoLev y iIn SNoLev x -> SNoEq_ (SNoLev y) x y -> nIn (SNoLev y) x -> P hyp ordinal (SNoLev x) claim ordinal (SNoLev y) -> P