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 ordinal : set prop const SNo : set prop axiom ordinal_SNo: !x:set.ordinal x -> SNo x const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom ordinal_In_SNoLt: !x:set.ordinal x -> !y:set.y iIn x -> y < x const nat_p : set prop const binintersect : set set set const SNoElts_ : set set const exp_SNo_nat : set set set const ordsucc : set set const Empty : set var x:set var f:set set var y:set var P:prop hyp ordinal (exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp nat_p (f (binintersect y (SNoElts_ x))) -> ordinal (f (binintersect y (SNoElts_ x))) -> SNo (f (binintersect y (SNoElts_ x))) -> f (binintersect y (SNoElts_ x)) < exp_SNo_nat (ordsucc (ordsucc Empty)) x -> P hyp f (binintersect y (SNoElts_ x)) iIn exp_SNo_nat (ordsucc (ordsucc Empty)) x hyp nat_p (f (binintersect y (SNoElts_ x))) claim ordinal (f (binintersect y (SNoElts_ x))) -> P