Search for blocks/addresses/...

Proofgold Asset

asset id
1bd5edca13ef5a88d214538e9e5496aebf9d6e0ee1ce581c81f1b298fa2dd966
asset hash
ce78df0b440e44633e4d75f3301623212e2ee1bdb2379e9817d8a3ddae139b73
bday / block
4882
tx
18c18..
preasset
doc published by Pr6Pc..
Definition FalseFalse := ∀ x0 : ο . x0
Theorem FalseEFalseE : False∀ x0 : ο . x0 (proof)
Definition TrueTrue := ∀ x0 : ο . x0x0
Theorem TrueITrueI : True (proof)
Definition notnot := λ x0 : ο . x0False
Theorem notInotI : ∀ x0 : ο . (x0False)not x0 (proof)
Theorem notEnotE : ∀ x0 : ο . not x0x0False (proof)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Theorem andIandI : ∀ x0 x1 : ο . x0x1and x0 x1 (proof)
Theorem andELandEL : ∀ x0 x1 : ο . and x0 x1x0 (proof)
Theorem andERandER : ∀ x0 x1 : ο . and x0 x1x1 (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Theorem orILorIL : ∀ x0 x1 : ο . x0or x0 x1 (proof)
Theorem orIRorIR : ∀ x0 x1 : ο . x1or x0 x1 (proof)
Theorem orEorE : ∀ x0 x1 x2 : ο . (x0x2)(x1x2)or x0 x1x2 (proof)
Theorem and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2 (proof)
Theorem and3Eand3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2∀ x3 : ο . (x0x1x2x3)x3 (proof)
Theorem or3I1or3I1 : ∀ x0 x1 x2 : ο . x0or (or x0 x1) x2 (proof)
Theorem or3I2or3I2 : ∀ x0 x1 x2 : ο . x1or (or x0 x1) x2 (proof)
Theorem or3I3or3I3 : ∀ x0 x1 x2 : ο . x2or (or x0 x1) x2 (proof)
Theorem or3Eor3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2∀ x3 : ο . (x0x3)(x1x3)(x2x3)x3 (proof)
Theorem and4Iand4I : ∀ x0 x1 x2 x3 : ο . x0x1x2x3and (and (and x0 x1) x2) x3 (proof)
Theorem and4Eand4E : ∀ x0 x1 x2 x3 : ο . and (and (and x0 x1) x2) x3∀ x4 : ο . (x0x1x2x3x4)x4 (proof)
Theorem or4I1or4I1 : ∀ x0 x1 x2 x3 : ο . x0or (or (or x0 x1) x2) x3 (proof)
Theorem or4I2or4I2 : ∀ x0 x1 x2 x3 : ο . x1or (or (or x0 x1) x2) x3 (proof)
Theorem or4I3or4I3 : ∀ x0 x1 x2 x3 : ο . x2or (or (or x0 x1) x2) x3 (proof)
Theorem or4I4or4I4 : ∀ x0 x1 x2 x3 : ο . x3or (or (or x0 x1) x2) x3 (proof)
Theorem or4Eor4E : ∀ x0 x1 x2 x3 : ο . or (or (or x0 x1) x2) x3∀ x4 : ο . (x0x4)(x1x4)(x2x4)(x3x4)x4 (proof)
Definition iffiff := λ x0 x1 : ο . and (x0x1) (x1x0)
Theorem iffELiffEL : ∀ x0 x1 : ο . iff x0 x1x0x1 (proof)
Theorem iffERiffER : ∀ x0 x1 : ο . iff x0 x1x1x0 (proof)
Theorem iffIiffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1 (proof)
Theorem iff_refliff_refl : ∀ x0 : ο . iff x0 x0 (proof)
Definition nInnIn := λ x0 x1 . not (x0x1)
Known Eps_i_axEps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1x0 (prim0 x0)
Theorem Eps_i_exEps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0) (proof)
Known prop_extprop_ext : ∀ x0 x1 : ο . iff x0 x1x0 = x1
Theorem pred_extpred_ext : ∀ x0 x1 : ι → ο . (∀ x2 . iff (x0 x2) (x1 x2))x0 = x1 (proof)
Theorem prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1 (proof)
Theorem pred_ext_2pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2x1 x2)(∀ x2 . x1 x2x0 x2)x0 = x1 (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Theorem Subq_refSubq_ref : ∀ x0 . x0x0 (proof)
Theorem Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2 (proof)
Theorem Subq_contraSubq_contra : ∀ x0 x1 x2 . x0x1nIn x2 x1nIn x2 x0 (proof)
Known EmptyAxEmptyAx : not (∀ x0 : ο . (∀ x1 . x10x0)x0)
Theorem EmptyEEmptyE : ∀ x0 . nIn x0 0 (proof)
Theorem Subq_EmptySubq_Empty : ∀ x0 . 0x0 (proof)
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Theorem Empty_Subq_eqEmpty_Subq_eq : ∀ x0 . x00x0 = 0 (proof)
Theorem Empty_eqEmpty_eq : ∀ x0 . (∀ x1 . nIn x1 x0)x0 = 0 (proof)
Known UnionEqUnionEq : ∀ x0 x1 . iff (x1prim3 x0) (∀ x2 : ο . (∀ x3 . and (x1x3) (x3x0)x2)x2)
Theorem UnionIUnionI : ∀ x0 x1 x2 . x1x2x2x0x1prim3 x0 (proof)
Theorem UnionEUnionE : ∀ x0 x1 . x1prim3 x0∀ x2 : ο . (∀ x3 . and (x1x3) (x3x0)x2)x2 (proof)
Theorem UnionE_impredUnionE_impred : ∀ x0 x1 . x1prim3 x0∀ x2 : ο . (∀ x3 . x1x3x3x0x2)x2 (proof)
Theorem Union_EmptyUnion_Empty : prim3 0 = 0 (proof)
Known PowerEqPowerEq : ∀ x0 x1 . iff (x1prim4 x0) (x1x0)
Theorem PowerEPowerE : ∀ x0 x1 . x1prim4 x0x1x0 (proof)
Theorem PowerIPowerI : ∀ x0 x1 . x1x0x1prim4 x0 (proof)
Theorem Power_SubqPower_Subq : ∀ x0 x1 . x0x1prim4 x0prim4 x1 (proof)
Theorem Empty_In_PowerEmpty_In_Power : ∀ x0 . 0prim4 x0 (proof)
Theorem Self_In_PowerSelf_In_Power : ∀ x0 . x0prim4 x0 (proof)
Theorem Union_Power_SubqUnion_Power_Subq : ∀ x0 . prim3 (prim4 x0)x0 (proof)
Theorem xmxm : ∀ x0 : ο . or x0 (not x0) (proof)
Theorem dnegdneg : ∀ x0 : ο . not (not x0)x0 (proof)
Theorem imp_not_orimp_not_or : ∀ x0 x1 : ο . (x0x1)or (not x0) x1 (proof)
Theorem not_and_or_demorgannot_and_or_demorgan : ∀ x0 x1 : ο . not (and x0 x1)or (not x0) (not x1) (proof)
Definition exactly1of2exactly1of2 := λ x0 x1 : ο . or (and x0 (not x1)) (and (not x0) x1)
Theorem exactly1of2_I1exactly1of2_I1 : ∀ x0 x1 : ο . x0not x1exactly1of2 x0 x1 (proof)
Theorem exactly1of2_I2exactly1of2_I2 : ∀ x0 x1 : ο . not x0x1exactly1of2 x0 x1 (proof)
Theorem exactly1of2_impI1exactly1of2_impI1 : ∀ x0 x1 : ο . (x0not x1)(not x0x1)exactly1of2 x0 x1 (proof)
Theorem exactly1of2_impI2exactly1of2_impI2 : ∀ x0 x1 : ο . (x1not x0)(not x1x0)exactly1of2 x0 x1 (proof)
Theorem exactly1of2_Eexactly1of2_E : ∀ x0 x1 : ο . exactly1of2 x0 x1∀ x2 : ο . (x0not x1x2)(not x0x1x2)x2 (proof)
Theorem exactly1of2_orexactly1of2_or : ∀ x0 x1 : ο . exactly1of2 x0 x1or x0 x1 (proof)
Theorem exactly1of2_impn12exactly1of2_impn12 : ∀ x0 x1 : ο . exactly1of2 x0 x1x0not x1 (proof)
Theorem exactly1of2_impn21exactly1of2_impn21 : ∀ x0 x1 : ο . exactly1of2 x0 x1x1not x0 (proof)
Theorem exactly1of2_nimp12exactly1of2_nimp12 : ∀ x0 x1 : ο . exactly1of2 x0 x1not x0x1 (proof)
Theorem exactly1of2_nimp21exactly1of2_nimp21 : ∀ x0 x1 : ο . exactly1of2 x0 x1not x1x0 (proof)
Definition exactly1of3exactly1of3 := λ x0 x1 x2 : ο . or (and (exactly1of2 x0 x1) (not x2)) (and (and (not x0) (not x1)) x2)
Theorem exactly1of3_I1exactly1of3_I1 : ∀ x0 x1 x2 : ο . x0not x1not x2exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_I2exactly1of3_I2 : ∀ x0 x1 x2 : ο . not x0x1not x2exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_I3exactly1of3_I3 : ∀ x0 x1 x2 : ο . not x0not x1x2exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_impI1exactly1of3_impI1 : ∀ x0 x1 x2 : ο . (x0not x1)(x0not x2)(x1not x2)(not x0or x1 x2)exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_impI2exactly1of3_impI2 : ∀ x0 x1 x2 : ο . (x1not x0)(x1not x2)(x0not x2)(not x1or x0 x2)exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_impI3exactly1of3_impI3 : ∀ x0 x1 x2 : ο . (x2not x0)(x2not x1)(x0not x1)(not x0x1)exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_Eexactly1of3_E : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2∀ x3 : ο . (x0not x1not x2x3)(not x0x1not x2x3)(not x0not x1x2x3)x3 (proof)
Theorem exactly1of3_orexactly1of3_or : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2or (or x0 x1) x2 (proof)
Theorem exactly1of3_impn12exactly1of3_impn12 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2x0not x1 (proof)
Theorem exactly1of3_impn13exactly1of3_impn13 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2x0not x2 (proof)
Theorem exactly1of3_impn21exactly1of3_impn21 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2x1not x0 (proof)
Theorem exactly1of3_impn23exactly1of3_impn23 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2x1not x2 (proof)
Theorem exactly1of3_impn31exactly1of3_impn31 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2x2not x0 (proof)
Theorem exactly1of3_impn32exactly1of3_impn32 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2x2not x1 (proof)
Theorem exactly1of3_nimp1exactly1of3_nimp1 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2not x0or x1 x2 (proof)
Theorem exactly1of3_nimp2exactly1of3_nimp2 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2not x1or x0 x2 (proof)
Theorem exactly1of3_nimp3exactly1of3_nimp3 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2not x2or x0 x1 (proof)
Known ReplEqReplEq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (x2prim5 x0 x1) (∀ x3 : ο . (∀ x4 . and (x4x0) (x2 = x1 x4)x3)x3)
Theorem ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1 (proof)
Theorem ReplEReplE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . and (x4x0) (x2 = x1 x4)x3)x3 (proof)
Theorem ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3 (proof)
Theorem Repl_EmptyRepl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0 (proof)
Theorem ReplEq_ext_subReplEq_ext_sub : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)prim5 x0 x1prim5 x0 x2 (proof)
Theorem ReplEq_extReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)prim5 x0 x1 = prim5 x0 x2 (proof)
Definition If_iIf_i := λ x0 : ο . λ x1 x2 . prim0 (λ x3 . or (and x0 (x3 = x1)) (and (not x0) (x3 = x2)))
Theorem If_i_correctIf_i_correct : ∀ x0 : ο . ∀ x1 x2 . or (and x0 (If_i x0 x1 x2 = x1)) (and (not x0) (If_i x0 x1 x2 = x2)) (proof)
Theorem If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2 (proof)
Theorem If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1 (proof)
Theorem If_i_orIf_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2) (proof)
Theorem If_i_etaIf_i_eta : ∀ x0 : ο . ∀ x1 . If_i x0 x1 x1 = x1 (proof)
Definition UPairUPair := λ x0 x1 . {If_i (0x2) x0 x1|x2 ∈ prim4 (prim4 0)}
Theorem UPairEUPairE : ∀ x0 x1 x2 . x0UPair x1 x2or (x0 = x1) (x0 = x2) (proof)
Theorem UPairI1UPairI1 : ∀ x0 x1 . x0UPair x0 x1 (proof)
Theorem UPairI2UPairI2 : ∀ x0 x1 . x1UPair x0 x1 (proof)
Theorem 93b47.. : ∀ x0 x1 . UPair x0 x1UPair x1 x0 (proof)
Theorem UPair_comUPair_com : ∀ x0 x1 . UPair x0 x1 = UPair x1 x0 (proof)
Definition SingSing := λ x0 . UPair x0 x0
Theorem SingISingI : ∀ x0 . x0Sing x0 (proof)
Theorem SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0 (proof)
Definition binunionbinunion := λ x0 x1 . prim3 (UPair x0 x1)
Theorem binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1 (proof)
Theorem binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1 (proof)
Theorem binunionEbinunionE : ∀ x0 x1 x2 . x2binunion x0 x1or (x2x0) (x2x1) (proof)
Definition SetAdjoinSetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Theorem Power_0_Sing_0Power_0_Sing_0 : prim4 0 = Sing 0 (proof)
Theorem Repl_UPairRepl_UPair : ∀ x0 : ι → ι . ∀ x1 x2 . prim5 (UPair x1 x2) x0 = UPair (x0 x1) (x0 x2) (proof)
Theorem Repl_SingRepl_Sing : ∀ x0 : ι → ι . ∀ x1 . prim5 (Sing x1) x0 = Sing (x0 x1) (proof)
Theorem ReplEq_ext_subReplEq_ext_sub : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)prim5 x0 x1prim5 x0 x2 (proof)
Theorem ReplEq_extReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)prim5 x0 x1 = prim5 x0 x2 (proof)
Definition famunionfamunion := λ x0 . λ x1 : ι → ι . prim3 (prim5 x0 x1)
Theorem famunionIfamunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2x0x3x1 x2x3famunion x0 x1 (proof)
Theorem famunionEfamunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2famunion x0 x1∀ x3 : ο . (∀ x4 . and (x4x0) (x2x1 x4)x3)x3 (proof)
Theorem famunionE_impredfamunionE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2famunion x0 x1∀ x3 : ο . (∀ x4 . x4x0x2x1 x4x3)x3 (proof)
Theorem UnionEq_famunionIdUnionEq_famunionId : ∀ x0 . prim3 x0 = famunion x0 (λ x2 . x2) (proof)
Theorem ReplEq_famunion_SingReplEq_famunion_Sing : ∀ x0 . ∀ x1 : ι → ι . prim5 x0 x1 = famunion x0 (λ x3 . Sing (x1 x3)) (proof)
Theorem Power_SingPower_Sing : ∀ x0 . prim4 (Sing x0) = UPair 0 (Sing x0) (proof)
Theorem Power_Sing_0Power_Sing_0 : prim4 (Sing 0) = UPair 0 (Sing 0) (proof)
Definition SepSep := λ x0 . λ x1 : ι → ο . If_i (∀ x2 : ο . (∀ x3 . and (x3x0) (x1 x3)x2)x2) {If_i (x1 x2) x2 (prim0 (λ x3 . and (x3x0) (x1 x3)))|x2 ∈ x0} 0
Theorem SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1 (proof)
Theorem SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2) (proof)
Theorem SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0 (proof)
Theorem SepE2SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x1 x2 (proof)
Theorem Sep_SubqSep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1x0 (proof)
Theorem Sep_In_PowerSep_In_Power : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1prim4 x0 (proof)
Definition ReplSepReplSep := λ x0 . λ x1 : ι → ο . prim5 (Sep x0 x1)
Theorem ReplSepIReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3x0x1 x3x2 x3ReplSep x0 x1 x2 (proof)
Theorem ReplSepEReplSepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3ReplSep x0 x1 x2∀ x4 : ο . (∀ x5 . and (and (x5x0) (x1 x5)) (x3 = x2 x5)x4)x4 (proof)
Theorem ReplSepE_impredReplSepE_impred : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3ReplSep x0 x1 x2∀ x4 : ο . (∀ x5 . x5x0x1 x5x3 = x2 x5x4)x4 (proof)
Definition ReplSep2ReplSep2 := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . λ x3 : ι → ι → ι . prim3 {ReplSep (x1 x4) (x2 x4) (x3 x4)|x4 ∈ x0}
Theorem ReplSep2IReplSep2I : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . x4x0∀ x5 . x5x1 x4x2 x4 x5x3 x4 x5ReplSep2 x0 x1 x2 x3 (proof)
Theorem ReplSep2E_impredReplSep2E_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . x4ReplSep2 x0 x1 x2 x3∀ x5 : ο . (∀ x6 . x6x0∀ x7 . x7x1 x6x2 x6 x7x4 = x3 x6 x7x5)x5 (proof)
Theorem ReplSep2EReplSep2E : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . x4ReplSep2 x0 x1 x2 x3∀ x5 : ο . (∀ x6 . and (x6x0) (∀ x7 : ο . (∀ x8 . and (x8x1 x6) (and (x2 x6 x8) (x4 = x3 x6 x8))x7)x7)x5)x5 (proof)
Theorem binunion_assobinunion_asso : ∀ x0 x1 x2 . binunion x0 (binunion x1 x2) = binunion (binunion x0 x1) x2 (proof)
Theorem binunion_com_Subqbinunion_com_Subq : ∀ x0 x1 . binunion x0 x1binunion x1 x0 (proof)
Theorem binunion_combinunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0 (proof)
Theorem binunion_idlbinunion_idl : ∀ x0 . binunion 0 x0 = x0 (proof)
Theorem binunion_idrbinunion_idr : ∀ x0 . binunion x0 0 = x0 (proof)
Theorem binunion_idembinunion_idem : ∀ x0 . binunion x0 x0 = x0 (proof)
Theorem binunion_Subq_1binunion_Subq_1 : ∀ x0 x1 . x0binunion x0 x1 (proof)
Theorem binunion_Subq_2binunion_Subq_2 : ∀ x0 x1 . x1binunion x0 x1 (proof)
Theorem binunion_Subq_minbinunion_Subq_min : ∀ x0 x1 x2 . x0x2x1x2binunion x0 x1x2 (proof)
Theorem Subq_binunion_eqSubq_binunion_eq : ∀ x0 x1 . x0x1 = (binunion x0 x1 = x1) (proof)
Theorem binunion_nIn_Ibinunion_nIn_I : ∀ x0 x1 x2 . nIn x2 x0nIn x2 x1nIn x2 (binunion x0 x1) (proof)
Theorem binunion_nIn_Ebinunion_nIn_E : ∀ x0 x1 x2 . nIn x2 (binunion x0 x1)and (nIn x2 x0) (nIn x2 x1) (proof)
Definition binintersectbinintersect := λ x0 x1 . {x2 ∈ x0|x2x1}
Theorem binintersectIbinintersectI : ∀ x0 x1 x2 . x2x0x2x1x2binintersect x0 x1 (proof)
Theorem binintersectEbinintersectE : ∀ x0 x1 x2 . x2binintersect x0 x1and (x2x0) (x2x1) (proof)
Theorem binintersectE1binintersectE1 : ∀ x0 x1 x2 . x2binintersect x0 x1x2x0 (proof)
Theorem binintersectE2binintersectE2 : ∀ x0 x1 x2 . x2binintersect x0 x1x2x1 (proof)
Theorem binintersect_Subq_1binintersect_Subq_1 : ∀ x0 x1 . binintersect x0 x1x0 (proof)
Theorem binintersect_Subq_2binintersect_Subq_2 : ∀ x0 x1 . binintersect x0 x1x1 (proof)
Theorem binintersect_Subq_eq_1binintersect_Subq_eq_1 : ∀ x0 x1 . x0x1binintersect x0 x1 = x0 (proof)
Theorem binintersect_Subq_maxbinintersect_Subq_max : ∀ x0 x1 x2 . x2x0x2x1x2binintersect x0 x1 (proof)
Theorem binintersect_assobinintersect_asso : ∀ x0 x1 x2 . binintersect x0 (binintersect x1 x2) = binintersect (binintersect x0 x1) x2 (proof)
Theorem binintersect_com_Subqbinintersect_com_Subq : ∀ x0 x1 . binintersect x0 x1binintersect x1 x0 (proof)
Theorem binintersect_combinintersect_com : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0 (proof)
Theorem binintersect_annilbinintersect_annil : ∀ x0 . binintersect 0 x0 = 0 (proof)
Theorem binintersect_annirbinintersect_annir : ∀ x0 . binintersect x0 0 = 0 (proof)
Theorem binintersect_idembinintersect_idem : ∀ x0 . binintersect x0 x0 = x0 (proof)
Theorem binintersect_binunion_distrbinintersect_binunion_distr : ∀ x0 x1 x2 . binintersect x0 (binunion x1 x2) = binunion (binintersect x0 x1) (binintersect x0 x2) (proof)
Theorem binunion_binintersect_distrbinunion_binintersect_distr : ∀ x0 x1 x2 . binunion x0 (binintersect x1 x2) = binintersect (binunion x0 x1) (binunion x0 x2) (proof)
Theorem Subq_binintersection_eqSubq_binintersection_eq : ∀ x0 x1 . x0x1 = (binintersect x0 x1 = x0) (proof)
Theorem binintersect_nIn_I1binintersect_nIn_I1 : ∀ x0 x1 x2 . nIn x2 x0nIn x2 (binintersect x0 x1) (proof)
Theorem binintersect_nIn_I2binintersect_nIn_I2 : ∀ x0 x1 x2 . nIn x2 x1nIn x2 (binintersect x0 x1) (proof)
Theorem binintersect_nIn_Ebinintersect_nIn_E : ∀ x0 x1 x2 . nIn x2 (binintersect x0 x1)or (nIn x2 x0) (nIn x2 x1) (proof)
Definition setminussetminus := λ x0 x1 . {x2 ∈ x0|nIn x2 x1}
Theorem setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1 (proof)
Theorem setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1) (proof)
Theorem setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0 (proof)
Theorem setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1 (proof)
Theorem setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0 (proof)
Theorem setminus_Subq_contrasetminus_Subq_contra : ∀ x0 x1 x2 . x2x1setminus x0 x1setminus x0 x2 (proof)
Theorem setminus_nIn_I1setminus_nIn_I1 : ∀ x0 x1 x2 . nIn x2 x0nIn x2 (setminus x0 x1) (proof)
Theorem setminus_nIn_I2setminus_nIn_I2 : ∀ x0 x1 x2 . x2x1nIn x2 (setminus x0 x1) (proof)
Theorem setminus_nIn_Esetminus_nIn_E : ∀ x0 x1 x2 . nIn x2 (setminus x0 x1)or (nIn x2 x0) (x2x1) (proof)
Theorem setminus_selfannihsetminus_selfannih : ∀ x0 . setminus x0 x0 = 0 (proof)
Theorem setminus_binintersectsetminus_binintersect : ∀ x0 x1 x2 . setminus x0 (binintersect x1 x2) = binunion (setminus x0 x1) (setminus x0 x2) (proof)
Theorem setminus_binunionsetminus_binunion : ∀ x0 x1 x2 . setminus x0 (binunion x1 x2) = setminus (setminus x0 x1) x2 (proof)
Theorem binintersect_setminusbinintersect_setminus : ∀ x0 x1 x2 . setminus (binintersect x0 x1) x2 = binintersect x0 (setminus x1 x2) (proof)
Theorem binunion_setminusbinunion_setminus : ∀ x0 x1 x2 . setminus (binunion x0 x1) x2 = binunion (setminus x0 x2) (setminus x1 x2) (proof)
Theorem setminus_setminussetminus_setminus : ∀ x0 x1 x2 . setminus x0 (setminus x1 x2) = binunion (setminus x0 x1) (binintersect x0 x2) (proof)
Theorem setminus_annilsetminus_annil : ∀ x0 . setminus 0 x0 = 0 (proof)
Theorem setminus_idrsetminus_idr : ∀ x0 . setminus x0 0 = x0 (proof)
Known In_indIn_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . x0 x1
Theorem In_irrefIn_irref : ∀ x0 . nIn x0 x0 (proof)
Theorem In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False (proof)
Theorem In_no3cycleIn_no3cycle : ∀ x0 x1 x2 . x0x1x1x2x2x0False (proof)
Definition ordsuccordsucc := λ x0 . binunion x0 (Sing x0)
Theorem ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0 (proof)
Theorem ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0 (proof)
Theorem ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0) (proof)
Theorem neq_0_ordsuccneq_0_ordsucc : ∀ x0 . 0 = ordsucc x0∀ x1 : ο . x1 (proof)
Theorem neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2 (proof)
Theorem neq_ordsucc_0neq_ordsucc_0 : ∀ x0 . ordsucc x0 = 0∀ x1 : ο . x1 (proof)
Theorem ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1 (proof)
Theorem In_0_1In_0_1 : 01 (proof)
Theorem In_0_2In_0_2 : 02 (proof)
Theorem In_1_2In_1_2 : 12 (proof)
Definition nat_pnat_p := λ x0 . ∀ x1 : ι → ο . x1 0(∀ x2 . x1 x2x1 (ordsucc x2))x1 x0
Theorem nat_0nat_0 : nat_p 0 (proof)
Theorem nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0) (proof)
Theorem nat_1nat_1 : nat_p 1 (proof)
Theorem nat_2nat_2 : nat_p 2 (proof)
Theorem nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0 (proof)
Theorem nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0 (proof)
Theorem nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1 (proof)
Theorem nat_invnat_inv : ∀ x0 . nat_p x0or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2)x1)x1) (proof)
Theorem nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1 (proof)
Theorem nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1 (proof)
Theorem nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0 (proof)
Theorem nat_ordsucc_transnat_ordsucc_trans : ∀ x0 . nat_p x0∀ x1 . x1ordsucc x0x1x0 (proof)
Theorem Union_ordsucc_eqUnion_ordsucc_eq : ∀ x0 . nat_p x0prim3 (ordsucc x0) = x0 (proof)
Definition Union_closedUnion_closed := λ x0 . ∀ x1 . x1x0prim3 x1x0
Definition Power_closedPower_closed := λ x0 . ∀ x1 . x1x0prim4 x1x0
Definition Repl_closedRepl_closed := λ x0 . ∀ x1 . x1x0∀ x2 : ι → ι . (∀ x3 . x3x1x2 x3x0)prim5 x1 x2x0
Definition ZF_closedZF_closed := λ x0 . and (and (Union_closed x0) (Power_closed x0)) (Repl_closed x0)
Theorem ZF_closed_IZF_closed_I : ∀ x0 . Union_closed x0Power_closed x0Repl_closed x0ZF_closed x0 (proof)
Theorem ZF_closed_EZF_closed_E : ∀ x0 . ZF_closed x0∀ x1 : ο . (Union_closed x0Power_closed x0Repl_closed x0x1)x1 (proof)
Theorem ZF_Union_closedZF_Union_closed : ∀ x0 . ZF_closed x0∀ x1 . x1x0prim3 x1x0 (proof)
Theorem ZF_Power_closedZF_Power_closed : ∀ x0 . ZF_closed x0∀ x1 . x1x0prim4 x1x0 (proof)
Theorem ZF_Repl_closedZF_Repl_closed : ∀ x0 . ZF_closed x0∀ x1 . x1x0∀ x2 : ι → ι . (∀ x3 . x3x1x2 x3x0)prim5 x1 x2x0 (proof)
Theorem ZF_UPair_closedZF_UPair_closed : ∀ x0 . ZF_closed x0∀ x1 . x1x0∀ x2 . x2x0UPair x1 x2x0 (proof)
Theorem ZF_Sing_closedZF_Sing_closed : ∀ x0 . ZF_closed x0∀ x1 . x1x0Sing x1x0 (proof)
Theorem ZF_binunion_closedZF_binunion_closed : ∀ x0 . ZF_closed x0∀ x1 . x1x0∀ x2 . x2x0binunion x1 x2x0 (proof)
Theorem ZF_ordsucc_closedZF_ordsucc_closed : ∀ x0 . ZF_closed x0∀ x1 . x1x0ordsucc x1x0 (proof)
Known UnivOf_InUnivOf_In : ∀ x0 . x0prim6 x0
Known UnivOf_ZF_closedUnivOf_ZF_closed : ∀ x0 . ZF_closed (prim6 x0)
Theorem nat_p_UnivOf_Emptynat_p_UnivOf_Empty : ∀ x0 . nat_p x0x0prim6 0 (proof)
Definition omegaomega := Sep (prim6 0) nat_p
Theorem omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0 (proof)
Theorem nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega (proof)
Theorem omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega (proof)
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Definition ordinalordinal := λ x0 . and (TransSet x0) (∀ x1 . x1x0TransSet x1)
Theorem ordinal_TransSetordinal_TransSet : ∀ x0 . ordinal x0TransSet x0 (proof)
Theorem ordinal_In_TransSetordinal_In_TransSet : ∀ x0 . ordinal x0∀ x1 . x1x0TransSet x1 (proof)
Theorem ordinal_Emptyordinal_Empty : ordinal 0 (proof)
Theorem ordinal_Heredordinal_Hered : ∀ x0 . ordinal x0∀ x1 . x1x0ordinal x1 (proof)
Theorem TransSet_ordsuccTransSet_ordsucc : ∀ x0 . TransSet x0TransSet (ordsucc x0) (proof)
Theorem ordinal_ordsuccordinal_ordsucc : ∀ x0 . ordinal x0ordinal (ordsucc x0) (proof)
Theorem nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0 (proof)
Theorem ordinal_1ordinal_1 : ordinal 1 (proof)
Theorem ordinal_2ordinal_2 : ordinal 2 (proof)
Theorem omega_TransSetomega_TransSet : TransSet omega (proof)
Theorem omega_ordinalomega_ordinal : ordinal omega (proof)
Theorem ordsucc_omega_ordinalordsucc_omega_ordinal : ordinal (ordsucc omega) (proof)
Theorem TransSet_ordsucc_In_SubqTransSet_ordsucc_In_Subq : ∀ x0 . TransSet x0∀ x1 . x1x0ordsucc x1x0 (proof)
Theorem ordinal_ordsucc_In_Subqordinal_ordsucc_In_Subq : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1x0 (proof)
Theorem ordinal_trichotomy_orordinal_trichotomy_or : ∀ x0 x1 . ordinal x0ordinal x1or (or (x0x1) (x0 = x1)) (x1x0) (proof)
Theorem ordinal_In_Or_Subqordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0ordinal x1or (x0x1) (x1x0) (proof)
Theorem ordinal_linearordinal_linear : ∀ x0 x1 . ordinal x0ordinal x1or (x0x1) (x1x0) (proof)
Theorem ordinal_ordsucc_In_eqordinal_ordsucc_In_eq : ∀ x0 x1 . ordinal x0x1x0or (ordsucc x1x0) (x0 = ordsucc x1) (proof)
Theorem ordinal_lim_or_succordinal_lim_or_succ : ∀ x0 . ordinal x0or (∀ x1 . x1x0ordsucc x1x0) (∀ x1 : ο . (∀ x2 . and (x2x0) (x0 = ordsucc x2)x1)x1) (proof)
Theorem ordinal_ordsucc_Inordinal_ordsucc_In : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1ordsucc x0 (proof)
Theorem ordinal_Unionordinal_Union : ∀ x0 . (∀ x1 . x1x0ordinal x1)ordinal (prim3 x0) (proof)
Theorem ordinal_famunionordinal_famunion : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2x0ordinal (x1 x2))ordinal (famunion x0 x1) (proof)
Theorem ordinal_binintersectordinal_binintersect : ∀ x0 x1 . ordinal x0ordinal x1ordinal (binintersect x0 x1) (proof)
Theorem ordinal_binunionordinal_binunion : ∀ x0 x1 . ordinal x0ordinal x1ordinal (binunion x0 x1) (proof)
Theorem ordinal_Sepordinal_Sep : ∀ x0 . ordinal x0∀ x1 : ι → ο . (∀ x2 . x2x0∀ x3 . x3x2x1 x2x1 x3)ordinal (Sep x0 x1) (proof)
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Definition surjsurj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Definition bijbij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Definition invinv := λ x0 . λ x1 : ι → ι . λ x2 . prim0 (λ x3 . and (x3x0) (x1 x3 = x2))
Theorem surj_rinvsurj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)∀ x3 . x3x1and (inv x0 x2 x3x0) (x2 (inv x0 x2 x3) = x3) (proof)
Theorem inj_linv_coddep : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)∀ x3 . x3x0inv x0 x2 (x2 x3) = x3 (proof)
Theorem bij_invbij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2bij x1 x0 (inv x0 x2) (proof)
Theorem bij_compbij_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . bij x0 x1 x3bij x1 x2 x4bij x0 x2 (λ x5 . x4 (x3 x5)) (proof)
Theorem bij_idbij_id : ∀ x0 . bij x0 x0 (λ x1 . x1) (proof)
Theorem bij_injbij_inj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2inj x0 x1 x2 (proof)
Theorem bij_surjbij_surj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2surj x0 x1 x2 (proof)
Theorem inj_surj_bijinj_surj_bij : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2surj x0 x1 x2bij x0 x1 x2 (proof)
Theorem surj_inv_injsurj_inv_inj : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)inj x1 x0 (inv x0 x2) (proof)
Definition atleastpatleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3x2)x2
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Definition finitefinite := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2omega) (equip x0 x2)x1)x1
Definition infiniteinfinite := λ x0 . not (finite x0)