const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y term PNoEq_ = \x:set.\p:set prop.\q:set prop.!y:set.y iIn x -> (p y <-> q y) const binunion : set set set const Sep : set (set prop) set const ReplSep : set (set prop) (set set) set const SetAdjoin : set set set const Sing : set set const ordsucc : set set const Empty : set term PSNo = \x:set.\p:set prop.binunion (Sep x p) (ReplSep x (\y:set.~ p y) \y:set.SetAdjoin y (Sing (ordsucc Empty))) axiom SepE2: !x:set.!p:set prop.!y:set.y iIn Sep x p -> p y const ordinal : set prop axiom tagged_notin_ordinal: !x:set.!y:set.ordinal x -> nIn (SetAdjoin y (Sing (ordsucc Empty))) x axiom ReplSepE_impred: !x:set.!p:set prop.!f:set set.!y:set.y iIn ReplSep x p f -> !P:prop.(!z:set.z iIn x -> p z -> y = f z -> P) -> P axiom FalseE: ~ False axiom binunionE: !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y axiom SepI: !x:set.!p:set prop.!y:set.y iIn x -> p y -> y iIn Sep x p axiom binunionI1: !x:set.!y:set.!z:set.z iIn x -> z iIn binunion x y axiom iffI: !P:prop.!Q:prop.(P -> Q) -> (Q -> P) -> (P <-> Q) claim !x:set.ordinal x -> !p:set prop.!y:set.y iIn x -> (y iIn PSNo x p <-> p y)