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 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 PNoLt_ = \x:set.\p:set prop.\q:set prop.?y:set.y iIn x & (PNoEq_ y p q & ~ p y & q y) 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 axiom PNoEq_antimon_: !p:set prop.!q:set prop.!x:set.ordinal x -> !y:set.y iIn x -> PNoEq_ x p q -> PNoEq_ y p q axiom PNoEq_tra_: !x:set.!p:set prop.!q:set prop.!p2:set prop.PNoEq_ x p q -> PNoEq_ x q p2 -> PNoEq_ x p p2 axiom iffEL: !P:prop.!Q:prop.(P <-> Q) -> P -> Q const PNoLt : set (set prop) set (set prop) prop axiom PNoLtI2: !x:set.!y:set.!p:set prop.!q:set prop.x iIn y -> PNoEq_ x p q -> q x -> PNoLt x p y q axiom FalseE: ~ False axiom PNoLtI3: !x:set.!y:set.!p:set prop.!q:set prop.y iIn x -> PNoEq_ y p q -> ~ p y -> PNoLt x p y q axiom ordinal_trichotomy_or: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | x = y | y iIn x 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 axiom binintersectI: !x:set.!y:set.!z:set.z iIn x -> z iIn y -> z iIn binintersect x y axiom PNoLtI1: !x:set.!y:set.!p:set prop.!q:set prop.PNoLt_ (binintersect x y) p q -> PNoLt x p y q lemma !x:set.!y:set.!z:set.!p:set prop.!q:set prop.!p2:set prop.!w:set.ordinal y -> ordinal z -> TransSet x -> TransSet z -> PNoLt y q z p2 -> w iIn x -> w iIn y -> PNoEq_ w p q -> ~ p w -> q w -> ordinal w -> PNoLt x p z p2 lemma !x:set.!y:set.!z:set.!p:set prop.!q:set prop.!p2:set prop.!w:set.ordinal x -> ordinal y -> TransSet z -> PNoEq_ x p q -> q x -> w iIn y -> w iIn z -> PNoEq_ w q p2 -> ~ q w -> p2 w -> ordinal w -> PNoLt x p z p2 claim !x:set.!y:set.!z:set.ordinal x -> ordinal y -> ordinal z -> !p:set prop.!q:set prop.!p2:set prop.PNoLt x p y q -> PNoLt y q z p2 -> PNoLt x p z p2