Proofgold Asset

Definition False^False := ∀ x0 : ο . x0
Theorem FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition True^True := ∀ x0 : ο . x0 ⟶ x0
Theorem TrueI^TrueI : True
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem notI^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Theorem notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem andEL^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Theorem andER^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem orE^orE : ∀ x0 x1 x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ or x0 x1 ⟶ x2
Theorem and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem and3E^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem or3I1^or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Theorem or3I2^or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Theorem or3I3^or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Theorem or3E^or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Theorem and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem and4E^and4E : ∀ x0 x1 x2 x3 : ο . and (and (and x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4) ⟶ x4
Theorem or4I1^or4I1 : ∀ x0 x1 x2 x3 : ο . x0 ⟶ or (or (or x0 x1) x2) x3
Theorem or4I2^or4I2 : ∀ x0 x1 x2 x3 : ο . x1 ⟶ or (or (or x0 x1) x2) x3
Theorem or4I3^or4I3 : ∀ x0 x1 x2 x3 : ο . x2 ⟶ or (or (or x0 x1) x2) x3
Theorem or4I4^or4I4 : ∀ x0 x1 x2 x3 : ο . x3 ⟶ or (or (or x0 x1) x2) x3
Theorem or4E^or4E : ∀ x0 x1 x2 x3 : ο . or (or (or x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x4) ⟶ (x1 ⟶ x4) ⟶ (x2 ⟶ x4) ⟶ (x3 ⟶ x4) ⟶ x4
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Theorem iffEL^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1
Theorem iffER^iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0
Theorem iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem iff_refl^iff_refl : ∀ x0 : ο . iff x0 x0
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known Eps_i_ax^Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Theorem Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Known prop_ext^prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Theorem pred_ext^pred_ext : ∀ x0 x1 : ι → ο . (∀ x2 . iff (x0 x2) (x1 x2)) ⟶ x0 = x1
Theorem prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem pred_ext_2^pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Theorem Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Theorem Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Theorem Subq_contra^Subq_contra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ nIn x2 x1 ⟶ nIn x2 x0
Known EmptyAx^EmptyAx : not (∀ x0 : ο . (∀ x1 . x1 ∈ 0 ⟶ x0) ⟶ x0)
Theorem EmptyE^EmptyE : ∀ x0 . nIn x0 0
Theorem Subq_Empty^Subq_Empty : ∀ x0 . 0 ⊆ x0
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Theorem Empty_Subq_eq^{Empty_Subq_eq} : ∀ x0 . x0 ⊆ 0 ⟶ x0 = 0
Theorem Empty_eq^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Known UnionEq^UnionEq : ∀ x0 x1 . iff (x1 ∈ prim3 x0) (∀ x2 : ο . (∀ x3 . and (x1 ∈ x3) (x3 ∈ x0) ⟶ x2) ⟶ x2)
Theorem UnionI^UnionI : ∀ x0 x1 x2 . x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ x1 ∈ prim3 x0
Theorem UnionE^UnionE : ∀ x0 x1 . x1 ∈ prim3 x0 ⟶ ∀ x2 : ο . (∀ x3 . and (x1 ∈ x3) (x3 ∈ x0) ⟶ x2) ⟶ x2
Theorem UnionE_impred^{UnionE_impred} : ∀ x0 x1 . x1 ∈ prim3 x0 ⟶ ∀ x2 : ο . (∀ x3 . x1 ∈ x3 ⟶ x3 ∈ x0 ⟶ x2) ⟶ x2
Theorem Union_Empty^Union_Empty : prim3 0 = 0
Known PowerEq^PowerEq : ∀ x0 x1 . iff (x1 ∈ prim4 x0) (x1 ⊆ x0)
Theorem PowerE^PowerE : ∀ x0 x1 . x1 ∈ prim4 x0 ⟶ x1 ⊆ x0
Theorem PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Theorem Power_Subq^Power_Subq : ∀ x0 x1 . x0 ⊆ x1 ⟶ prim4 x0 ⊆ prim4 x1
Theorem Empty_In_Power^{Empty_In_Power} : ∀ x0 . 0 ∈ prim4 x0
Theorem Self_In_Power^{Self_In_Power} : ∀ x0 . x0 ∈ prim4 x0
Theorem Union_Power_Subq^{Union_Power_Subq} : ∀ x0 . prim3 (prim4 x0) ⊆ x0
Theorem xm^xm : ∀ x0 : ο . or x0 (not x0)
Theorem dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem imp_not_or^imp_not_or : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ or (not x0) x1
Theorem not_and_or_demorgan^{not_and_or_demorgan} : ∀ x0 x1 : ο . not (and x0 x1) ⟶ or (not x0) (not x1)
Definition exactly1of2^exactly1of2 := λ x0 x1 : ο . or (and x0 (not x1)) (and (not x0) x1)
Theorem exactly1of2_I1^{exactly1of2_I1} : ∀ x0 x1 : ο . x0 ⟶ not x1 ⟶ exactly1of2 x0 x1
Theorem exactly1of2_I2^{exactly1of2_I2} : ∀ x0 x1 : ο . not x0 ⟶ x1 ⟶ exactly1of2 x0 x1
Theorem exactly1of2_impI1^{exactly1of2_impI1} : ∀ x0 x1 : ο . (x0 ⟶ not x1) ⟶ (not x0 ⟶ x1) ⟶ exactly1of2 x0 x1
Theorem exactly1of2_impI2^{exactly1of2_impI2} : ∀ x0 x1 : ο . (x1 ⟶ not x0) ⟶ (not x1 ⟶ x0) ⟶ exactly1of2 x0 x1
Theorem exactly1of2_E^{exactly1of2_E} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ not x1 ⟶ x2) ⟶ (not x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem exactly1of2_or^{exactly1of2_or} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ or x0 x1
Theorem exactly1of2_impn12^{exactly1of2_impn12} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ x0 ⟶ not x1
Theorem exactly1of2_impn21^{exactly1of2_impn21} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ x1 ⟶ not x0
Theorem exactly1of2_nimp12^{exactly1of2_nimp12} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ not x0 ⟶ x1
Theorem exactly1of2_nimp21^{exactly1of2_nimp21} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ not x1 ⟶ x0
Definition exactly1of3^exactly1of3 := λ x0 x1 x2 : ο . or (and (exactly1of2 x0 x1) (not x2)) (and (and (not x0) (not x1)) x2)
Theorem exactly1of3_I1^{exactly1of3_I1} : ∀ x0 x1 x2 : ο . x0 ⟶ not x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2
Theorem exactly1of3_I2^{exactly1of3_I2} : ∀ x0 x1 x2 : ο . not x0 ⟶ x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2
Theorem exactly1of3_I3^{exactly1of3_I3} : ∀ x0 x1 x2 : ο . not x0 ⟶ not x1 ⟶ x2 ⟶ exactly1of3 x0 x1 x2
Theorem exactly1of3_impI1^{exactly1of3_impI1} : ∀ x0 x1 x2 : ο . (x0 ⟶ not x1) ⟶ (x0 ⟶ not x2) ⟶ (x1 ⟶ not x2) ⟶ (not x0 ⟶ or x1 x2) ⟶ exactly1of3 x0 x1 x2
Theorem exactly1of3_impI2^{exactly1of3_impI2} : ∀ x0 x1 x2 : ο . (x1 ⟶ not x0) ⟶ (x1 ⟶ not x2) ⟶ (x0 ⟶ not x2) ⟶ (not x1 ⟶ or x0 x2) ⟶ exactly1of3 x0 x1 x2
Theorem exactly1of3_impI3^{exactly1of3_impI3} : ∀ x0 x1 x2 : ο . (x2 ⟶ not x0) ⟶ (x2 ⟶ not x1) ⟶ (x0 ⟶ not x1) ⟶ (not x0 ⟶ x1) ⟶ exactly1of3 x0 x1 x2
Theorem exactly1of3_E^{exactly1of3_E} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ ∀ x3 : ο . (x0 ⟶ not x1 ⟶ not x2 ⟶ x3) ⟶ (not x0 ⟶ x1 ⟶ not x2 ⟶ x3) ⟶ (not x0 ⟶ not x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem exactly1of3_or^{exactly1of3_or} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ or (or x0 x1) x2
Theorem exactly1of3_impn12^{exactly1of3_impn12} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x0 ⟶ not x1
Theorem exactly1of3_impn13^{exactly1of3_impn13} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x0 ⟶ not x2
Theorem exactly1of3_impn21^{exactly1of3_impn21} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x1 ⟶ not x0
Theorem exactly1of3_impn23^{exactly1of3_impn23} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x1 ⟶ not x2
Theorem exactly1of3_impn31^{exactly1of3_impn31} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x2 ⟶ not x0
Theorem exactly1of3_impn32^{exactly1of3_impn32} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x2 ⟶ not x1
Theorem exactly1of3_nimp1^{exactly1of3_nimp1} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ not x0 ⟶ or x1 x2
Theorem exactly1of3_nimp2^{exactly1of3_nimp2} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ not x1 ⟶ or x0 x2
Theorem exactly1of3_nimp3^{exactly1of3_nimp3} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ not x2 ⟶ or x0 x1
Known ReplEq^ReplEq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (x2 ∈ prim5 x0 x1) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = x1 x4) ⟶ x3) ⟶ x3)
Theorem ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Theorem ReplE^ReplE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = x1 x4) ⟶ x3) ⟶ x3
Theorem ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem Repl_Empty^Repl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0
Theorem ReplEq_ext_sub^{ReplEq_ext_sub} : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 ⊆ prim5 x0 x2
Theorem ReplEq_ext^ReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 = prim5 x0 x2
Definition If_i^If_i := λ x0 : ο . λ x1 x2 . prim0 (λ x3 . or (and x0 (x3 = x1)) (and (not x0) (x3 = x2)))
Theorem If_i_correct^If_i_correct : ∀ x0 : ο . ∀ x1 x2 . or (and x0 (If_i x0 x1 x2 = x1)) (and (not x0) (If_i x0 x1 x2 = x2))
Theorem If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem If_i_or^If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2)
Theorem If_i_eta^If_i_eta : ∀ x0 : ο . ∀ x1 . If_i x0 x1 x1 = x1
Definition UPair^UPair := λ x0 x1 . {If_i (0 ∈ x2) x0 x1|x2 ∈ prim4 (prim4 0)}
Theorem UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Theorem UPairI1^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Theorem UPairI2^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Theorem 93b47.. : ∀ x0 x1 . UPair x0 x1 ⊆ UPair x1 x0
Theorem UPair_com^UPair_com : ∀ x0 x1 . UPair x0 x1 = UPair x1 x0
Definition Sing^Sing := λ x0 . UPair x0 x0
Theorem SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Theorem SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Definition binunion^binunion := λ x0 x1 . prim3 (UPair x0 x1)
Theorem binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Theorem binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Theorem binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Theorem Power_0_Sing_0^{Power_0_Sing_0} : prim4 0 = Sing 0
Theorem Repl_UPair^Repl_UPair : ∀ x0 : ι → ι . ∀ x1 x2 . prim5 (UPair x1 x2) x0 = UPair (x0 x1) (x0 x2)
Theorem Repl_Sing^Repl_Sing : ∀ x0 : ι → ι . ∀ x1 . prim5 (Sing x1) x0 = Sing (x0 x1)
Theorem ReplEq_ext_sub^{ReplEq_ext_sub} : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 ⊆ prim5 x0 x2
Theorem ReplEq_ext^ReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 = prim5 x0 x2
Definition famunion^famunion := λ x0 . λ x1 : ι → ι . prim3 (prim5 x0 x1)
Theorem famunionI^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ x0 ⟶ x3 ∈ x1 x2 ⟶ x3 ∈ famunion x0 x1
Theorem famunionE^famunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 ∈ x1 x4) ⟶ x3) ⟶ x3
Theorem famunionE_impred^{famunionE_impred} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 ∈ x1 x4 ⟶ x3) ⟶ x3
Theorem UnionEq_famunionId^{UnionEq_famunionId} : ∀ x0 . prim3 x0 = famunion x0 (λ x2 . x2)
Theorem ReplEq_famunion_Sing^{ReplEq_famunion_Sing} : ∀ x0 . ∀ x1 : ι → ι . prim5 x0 x1 = famunion x0 (λ x3 . Sing (x1 x3))
Theorem Power_Sing^Power_Sing : ∀ x0 . prim4 (Sing x0) = UPair 0 (Sing x0)
Theorem Power_Sing_0^Power_Sing_0 : prim4 (Sing 0) = UPair 0 (Sing 0)
Definition Sep^Sep := λ x0 . λ x1 : ι → ο . If_i (∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (x1 x3) ⟶ x2) ⟶ x2) {If_i (x1 x2) x2 (prim0 (λ x3 . and (x3 ∈ x0) (x1 x3)))|x2 ∈ x0} 0
Theorem SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Theorem SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Theorem SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Theorem SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Theorem Sep_Subq^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ⊆ x0
Theorem Sep_In_Power^Sep_In_Power : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ∈ prim4 x0
Definition ReplSep^ReplSep := λ x0 . λ x1 : ι → ο . prim5 (Sep x0 x1)
Theorem ReplSepI^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⟶ x2 x3 ∈ ReplSep x0 x1 x2
Theorem ReplSepE^ReplSepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ ReplSep x0 x1 x2 ⟶ ∀ x4 : ο . (∀ x5 . and (and (x5 ∈ x0) (x1 x5)) (x3 = x2 x5) ⟶ x4) ⟶ x4
Theorem ReplSepE_impred^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ ReplSep x0 x1 x2 ⟶ ∀ x4 : ο . (∀ x5 . x5 ∈ x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Definition ReplSep2^ReplSep2 := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . λ x3 : ι → ι → ι . prim3 {ReplSep (x1 x4) (x2 x4) (x3 x4)|x4 ∈ x0}
Theorem ReplSep2I^ReplSep2I : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 x4 ⟶ x2 x4 x5 ⟶ x3 x4 x5 ∈ ReplSep2 x0 x1 x2 x3
Theorem ReplSep2E_impred^{ReplSep2E_impred} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . x4 ∈ ReplSep2 x0 x1 x2 x3 ⟶ ∀ x5 : ο . (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x1 x6 ⟶ x2 x6 x7 ⟶ x4 = x3 x6 x7 ⟶ x5) ⟶ x5
Theorem ReplSep2E^ReplSep2E : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . x4 ∈ ReplSep2 x0 x1 x2 x3 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (∀ x7 : ο . (∀ x8 . and (x8 ∈ x1 x6) (and (x2 x6 x8) (x4 = x3 x6 x8)) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5
Theorem binunion_asso^{binunion_asso} : ∀ x0 x1 x2 . binunion x0 (binunion x1 x2) = binunion (binunion x0 x1) x2
Theorem binunion_com_Subq^{binunion_com_Subq} : ∀ x0 x1 . binunion x0 x1 ⊆ binunion x1 x0
Theorem binunion_com^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Theorem binunion_idl^binunion_idl : ∀ x0 . binunion 0 x0 = x0
Theorem binunion_idr^binunion_idr : ∀ x0 . binunion x0 0 = x0
Theorem binunion_idem^{binunion_idem} : ∀ x0 . binunion x0 x0 = x0
Theorem binunion_Subq_1^{binunion_Subq_1} : ∀ x0 x1 . x0 ⊆ binunion x0 x1
Theorem binunion_Subq_2^{binunion_Subq_2} : ∀ x0 x1 . x1 ⊆ binunion x0 x1
Theorem binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Theorem Subq_binunion_eq^{Subq_binunion_eq} : ∀ x0 x1 . x0 ⊆ x1 = (binunion x0 x1 = x1)
Theorem binunion_nIn_I^{binunion_nIn_I} : ∀ x0 x1 x2 . nIn x2 x0 ⟶ nIn x2 x1 ⟶ nIn x2 (binunion x0 x1)
Theorem binunion_nIn_E^{binunion_nIn_E} : ∀ x0 x1 x2 . nIn x2 (binunion x0 x1) ⟶ and (nIn x2 x0) (nIn x2 x1)
Definition binintersect^binintersect := λ x0 x1 . {x2 ∈ x0|x2 ∈ x1}
Theorem binintersectI^{binintersectI} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ x1 ⟶ x2 ∈ binintersect x0 x1
Theorem binintersectE^{binintersectE} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ and (x2 ∈ x0) (x2 ∈ x1)
Theorem binintersectE1^{binintersectE1} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x0
Theorem binintersectE2^{binintersectE2} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x1
Theorem binintersect_Subq_1^{binintersect_Subq_1} : ∀ x0 x1 . binintersect x0 x1 ⊆ x0
Theorem binintersect_Subq_2^{binintersect_Subq_2} : ∀ x0 x1 . binintersect x0 x1 ⊆ x1
Theorem binintersect_Subq_eq_1^{binintersect_Subq_eq_1} : ∀ x0 x1 . x0 ⊆ x1 ⟶ binintersect x0 x1 = x0
Theorem binintersect_Subq_max^{binintersect_Subq_max} : ∀ x0 x1 x2 . x2 ⊆ x0 ⟶ x2 ⊆ x1 ⟶ x2 ⊆ binintersect x0 x1
Theorem binintersect_asso^{binintersect_asso} : ∀ x0 x1 x2 . binintersect x0 (binintersect x1 x2) = binintersect (binintersect x0 x1) x2
Theorem binintersect_com_Subq^{binintersect_com_Subq} : ∀ x0 x1 . binintersect x0 x1 ⊆ binintersect x1 x0
Theorem binintersect_com^{binintersect_com} : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0
Theorem binintersect_annil^{binintersect_annil} : ∀ x0 . binintersect 0 x0 = 0
Theorem binintersect_annir^{binintersect_annir} : ∀ x0 . binintersect x0 0 = 0
Theorem binintersect_idem^{binintersect_idem} : ∀ x0 . binintersect x0 x0 = x0
Theorem binintersect_binunion_distr^{binintersect_binunion_distr} : ∀ x0 x1 x2 . binintersect x0 (binunion x1 x2) = binunion (binintersect x0 x1) (binintersect x0 x2)
Theorem binunion_binintersect_distr^{binunion_binintersect_distr} : ∀ x0 x1 x2 . binunion x0 (binintersect x1 x2) = binintersect (binunion x0 x1) (binunion x0 x2)
Theorem Subq_binintersection_eq^{Subq_binintersection_eq} : ∀ x0 x1 . x0 ⊆ x1 = (binintersect x0 x1 = x0)
Theorem binintersect_nIn_I1^{binintersect_nIn_I1} : ∀ x0 x1 x2 . nIn x2 x0 ⟶ nIn x2 (binintersect x0 x1)
Theorem binintersect_nIn_I2^{binintersect_nIn_I2} : ∀ x0 x1 x2 . nIn x2 x1 ⟶ nIn x2 (binintersect x0 x1)
Theorem binintersect_nIn_E^{binintersect_nIn_E} : ∀ x0 x1 x2 . nIn x2 (binintersect x0 x1) ⟶ or (nIn x2 x0) (nIn x2 x1)
Definition setminus^setminus := λ x0 x1 . {x2 ∈ x0|nIn x2 x1}
Theorem setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Theorem setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Theorem setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Theorem setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Theorem setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Theorem setminus_Subq_contra^{setminus_Subq_contra} : ∀ x0 x1 x2 . x2 ⊆ x1 ⟶ setminus x0 x1 ⊆ setminus x0 x2
Theorem setminus_nIn_I1^{setminus_nIn_I1} : ∀ x0 x1 x2 . nIn x2 x0 ⟶ nIn x2 (setminus x0 x1)
Theorem setminus_nIn_I2^{setminus_nIn_I2} : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ nIn x2 (setminus x0 x1)
Theorem setminus_nIn_E^{setminus_nIn_E} : ∀ x0 x1 x2 . nIn x2 (setminus x0 x1) ⟶ or (nIn x2 x0) (x2 ∈ x1)
Theorem setminus_selfannih^{setminus_selfannih} : ∀ x0 . setminus x0 x0 = 0
Theorem setminus_binintersect^{setminus_binintersect} : ∀ x0 x1 x2 . setminus x0 (binintersect x1 x2) = binunion (setminus x0 x1) (setminus x0 x2)
Theorem setminus_binunion^{setminus_binunion} : ∀ x0 x1 x2 . setminus x0 (binunion x1 x2) = setminus (setminus x0 x1) x2
Theorem binintersect_setminus^{binintersect_setminus} : ∀ x0 x1 x2 . setminus (binintersect x0 x1) x2 = binintersect x0 (setminus x1 x2)
Theorem binunion_setminus^{binunion_setminus} : ∀ x0 x1 x2 . setminus (binunion x0 x1) x2 = binunion (setminus x0 x2) (setminus x1 x2)
Theorem setminus_setminus^{setminus_setminus} : ∀ x0 x1 x2 . setminus x0 (setminus x1 x2) = binunion (setminus x0 x1) (binintersect x0 x2)
Theorem setminus_annil^{setminus_annil} : ∀ x0 . setminus 0 x0 = 0
Theorem setminus_idr^setminus_idr : ∀ x0 . setminus x0 0 = x0
Known In_ind^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem In_irref^In_irref : ∀ x0 . nIn x0 x0
Theorem In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Theorem In_no3cycle^In_no3cycle : ∀ x0 x1 x2 . x0 ∈ x1 ⟶ x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ False
Definition ordsucc^ordsucc := λ x0 . binunion x0 (Sing x0)
Theorem ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Theorem ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Theorem neq_0_ordsucc^{neq_0_ordsucc} : ∀ x0 . 0 = ordsucc x0 ⟶ ∀ x1 : ο . x1
Theorem neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Theorem neq_ordsucc_0^{neq_ordsucc_0} : ∀ x0 . ordsucc x0 = 0 ⟶ ∀ x1 : ο . x1
Theorem ordsucc_inj^ordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1 ⟶ x0 = x1
Theorem In_0_1^In_0_1 : 0 ∈ 1
Theorem In_0_2^In_0_2 : 0 ∈ 2
Theorem In_1_2^In_1_2 : 1 ∈ 2
Definition nat_p^nat_p := λ x0 . ∀ x1 : ι → ο . x1 0 ⟶ (∀ x2 . x1 x2 ⟶ x1 (ordsucc x2)) ⟶ x1 x0
Theorem nat_0^nat_0 : nat_p 0
Theorem nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem nat_1^nat_1 : nat_p 1
Theorem nat_2^nat_2 : nat_p 2
Theorem nat_0_in_ordsucc^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Theorem nat_ordsucc_in_ordsucc^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Theorem nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Theorem nat_inv^nat_inv : ∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)
Theorem nat_complete_ind^{nat_complete_ind} : ∀ x0 : ι → ο . (∀ x1 . nat_p x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Theorem nat_p_trans^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Theorem nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Theorem nat_ordsucc_trans^{nat_ordsucc_trans} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ ordsucc x0 ⟶ x1 ⊆ x0
Theorem Union_ordsucc_eq^{Union_ordsucc_eq} : ∀ x0 . nat_p x0 ⟶ prim3 (ordsucc x0) = x0
Definition Union_closed^Union_closed := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ prim3 x1 ∈ x0
Definition Power_closed^Power_closed := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ prim4 x1 ∈ x0
Definition Repl_closed^Repl_closed := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0) ⟶ prim5 x1 x2 ∈ x0
Definition ZF_closed^ZF_closed := λ x0 . and (and (Union_closed x0) (Power_closed x0)) (Repl_closed x0)
Theorem ZF_closed_I^ZF_closed_I : ∀ x0 . Union_closed x0 ⟶ Power_closed x0 ⟶ Repl_closed x0 ⟶ ZF_closed x0
Theorem ZF_closed_E^ZF_closed_E : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 : ο . (Union_closed x0 ⟶ Power_closed x0 ⟶ Repl_closed x0 ⟶ x1) ⟶ x1
Theorem ZF_Union_closed^{ZF_Union_closed} : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ prim3 x1 ∈ x0
Theorem ZF_Power_closed^{ZF_Power_closed} : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ prim4 x1 ∈ x0
Theorem ZF_Repl_closed^{ZF_Repl_closed} : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0) ⟶ prim5 x1 x2 ∈ x0
Theorem ZF_UPair_closed^{ZF_UPair_closed} : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ UPair x1 x2 ∈ x0
Theorem ZF_Sing_closed^{ZF_Sing_closed} : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ Sing x1 ∈ x0
Theorem ZF_binunion_closed^{ZF_binunion_closed} : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ binunion x1 x2 ∈ x0
Theorem ZF_ordsucc_closed^{ZF_ordsucc_closed} : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ x0
Known UnivOf_In^UnivOf_In : ∀ x0 . x0 ∈ prim6 x0
Known UnivOf_ZF_closed^{UnivOf_ZF_closed} : ∀ x0 . ZF_closed (prim6 x0)
Theorem nat_p_UnivOf_Empty^{nat_p_UnivOf_Empty} : ∀ x0 . nat_p x0 ⟶ x0 ∈ prim6 0
Definition omega^omega := Sep (prim6 0) nat_p
Theorem omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Theorem nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Theorem omega_ordsucc^{omega_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ ordsucc x0 ∈ omega
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Definition ordinal^ordinal := λ x0 . and (TransSet x0) (∀ x1 . x1 ∈ x0 ⟶ TransSet x1)
Theorem ordinal_TransSet^{ordinal_TransSet} : ∀ x0 . ordinal x0 ⟶ TransSet x0
Theorem ordinal_In_TransSet^{ordinal_In_TransSet} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ TransSet x1
Theorem ordinal_Empty^{ordinal_Empty} : ordinal 0
Theorem ordinal_Hered^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordinal x1
Theorem TransSet_ordsucc^{TransSet_ordsucc} : ∀ x0 . TransSet x0 ⟶ TransSet (ordsucc x0)
Theorem ordinal_ordsucc^{ordinal_ordsucc} : ∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0)
Theorem nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Theorem ordinal_1^ordinal_1 : ordinal 1
Theorem ordinal_2^ordinal_2 : ordinal 2
Theorem omega_TransSet^{omega_TransSet} : TransSet omega
Theorem omega_ordinal^{omega_ordinal} : ordinal omega
Theorem ordsucc_omega_ordinal^{ordsucc_omega_ordinal} : ordinal (ordsucc omega)
Theorem TransSet_ordsucc_In_Subq^{TransSet_ordsucc_In_Subq} : ∀ x0 . TransSet x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ⊆ x0
Theorem ordinal_ordsucc_In_Subq^{ordinal_ordsucc_In_Subq} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ⊆ x0
Theorem ordinal_trichotomy_or^{ordinal_trichotomy_or} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (x0 ∈ x1) (x0 = x1)) (x1 ∈ x0)
Theorem ordinal_In_Or_Subq^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ∈ x1) (x1 ⊆ x0)
Theorem ordinal_linear^{ordinal_linear} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ⊆ x1) (x1 ⊆ x0)
Theorem ordinal_ordsucc_In_eq^{ordinal_ordsucc_In_eq} : ∀ x0 x1 . ordinal x0 ⟶ x1 ∈ x0 ⟶ or (ordsucc x1 ∈ x0) (x0 = ordsucc x1)
Theorem ordinal_lim_or_succ^{ordinal_lim_or_succ} : ∀ x0 . ordinal x0 ⟶ or (∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ x0) (∀ x1 : ο . (∀ x2 . and (x2 ∈ x0) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)
Theorem ordinal_ordsucc_In^{ordinal_ordsucc_In} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Theorem ordinal_Union^{ordinal_Union} : ∀ x0 . (∀ x1 . x1 ∈ x0 ⟶ ordinal x1) ⟶ ordinal (prim3 x0)
Theorem ordinal_famunion^{ordinal_famunion} : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ordinal (x1 x2)) ⟶ ordinal (famunion x0 x1)
Theorem ordinal_binintersect^{ordinal_binintersect} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (binintersect x0 x1)
Theorem ordinal_binunion^{ordinal_binunion} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (binunion x0 x1)
Theorem ordinal_Sep^ordinal_Sep : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x2 ⟶ x1 x2 ⟶ x1 x3) ⟶ ordinal (Sep x0 x1)
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition surj^surj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition inv^inv := λ x0 . λ x1 : ι → ι . λ x2 . prim0 (λ x3 . and (x3 ∈ x0) (x1 x3 = x2))
Theorem surj_rinv^surj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ ∀ x3 . x3 ∈ x1 ⟶ and (inv x0 x2 x3 ∈ x0) (x2 (inv x0 x2 x3) = x3)
Theorem inj_linv_coddep : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ ∀ x3 . x3 ∈ x0 ⟶ inv x0 x2 (x2 x3) = x3
Theorem bij_inv^bij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ bij x1 x0 (inv x0 x2)
Theorem bij_comp^bij_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . bij x0 x1 x3 ⟶ bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5))
Theorem bij_id^bij_id : ∀ x0 . bij x0 x0 (λ x1 . x1)
Theorem bij_inj^bij_inj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ inj x0 x1 x2
Theorem bij_surj^bij_surj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ surj x0 x1 x2
Theorem inj_surj_bij^inj_surj_bij : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ surj x0 x1 x2 ⟶ bij x0 x1 x2
Theorem surj_inv_inj^surj_inv_inj : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ inj x1 x0 (inv x0 x2)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Definition finite^finite := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (equip x0 x2) ⟶ x1) ⟶ x1
Definition infinite^infinite := λ x0 . not (finite x0)