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 const omega : set term finite = \x:set.?y:set.y iIn omega & equip x y term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term nIn = \x:set.\y:set.~ x iIn y const nat_p : set prop axiom nat_p_omega: !x:set.nat_p x -> x iIn omega const ordsucc : set set axiom ordsuccI2: !x:set.x iIn ordsucc x axiom ordsuccI1: !x:set.Subq x (ordsucc x) axiom In_irref: !x:set.nIn x x 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 binunion : set set set const Sing : set set var p:set prop var x:set var y:set var f:set set hyp !z:set.!w:set.finite z -> nIn w z -> p z -> p (binunion z (Sing w)) hyp nat_p x hyp !z:set.equip z x -> p z hyp !z:set.z iIn ordsucc x -> !w:set.w iIn ordsucc x -> f z = f w -> z = w hyp y = binunion (Repl x f) (Sing (f x)) claim equip (Repl x f) x -> p y