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 Sing : set set axiom SingE: !x:set.!y:set.y iIn Sing x -> y = x const binunion : set set set axiom binunionE: !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y axiom binunion_Subq_1: !x:set.!y:set.Subq x (binunion x y) axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y const ordsucc : set set axiom omega_ordsucc: !x:set.x iIn omega -> ordsucc x iIn omega const If_i : prop set set set axiom If_i_1: !P:prop.!x:set.!y:set.P -> If_i P x y = x axiom In_irref: !x:set.nIn x x axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y axiom equip_sym: !x:set.!y:set.equip x y -> equip y x axiom xm: !P:prop.P | ~ P axiom bijE: !x:set.!y:set.!f:set set.bij x y f -> !P:prop.((!z:set.z iIn x -> f z iIn y) -> (!z:set.z iIn x -> !w:set.w iIn x -> f z = f w -> z = w) -> (!z:set.z iIn y -> ?w:set.w iIn x & f w = z) -> P) -> P lemma !x:set.!y:set.finite x -> y iIn x -> binunion x (Sing y) = x -> finite (binunion x (Sing y)) lemma !x:set.!y:set.!z:set.!f:set set.(!w:set.w iIn z -> f w iIn x) -> (!w:set.w iIn z -> !u:set.u iIn z -> f w = f u -> w = u) -> (!w:set.w iIn x -> ?u:set.u iIn z & f u = w) -> nIn y x -> (?f2:set set.(!w:set.w iIn z -> f2 w = f w) & f2 z = y) -> ?f2:set set.bij (ordsucc z) (binunion x (Sing y)) f2 claim !x:set.!y:set.finite x -> finite (binunion x (Sing y))