Search for blocks/addresses/...

Proofgold Address

address
PUTiyKCE9m4RhxGJdqtT8WsKV2u8AcA3dPo
total
0
mg
-
conjpub
-
current assets
c86e5../6fdf1.. bday: 29812 doc published by PrQUS..
Param In_rec_iIn_rec_i : (ι(ιι) → ι) → ιι
Definition famunionfamunion := λ x0 . λ x1 : ι → ι . prim3 (prim5 x0 x1)
Definition V_ := In_rec_i (λ x0 . λ x1 : ι → ι . famunion x0 (λ x2 . prim4 (x1 x2)))
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known In_rec_i_eqIn_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_i x0 x1 = x0 x1 (In_rec_i x0)
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known famunionEfamunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2famunion x0 x1∀ x3 : ο . (∀ x4 . and (x4x0) (x2x1 x4)x3)x3
Known famunionIfamunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2x0x3x1 x2x3famunion x0 x1
Theorem V_eq : ∀ x0 . V_ x0 = famunion x0 (λ x2 . prim4 (V_ x2)) (proof)
Known PowerIPowerI : ∀ x0 x1 . x1x0x1prim4 x0
Theorem V_I : ∀ x0 x1 x2 . x1x2x0V_ x1x0V_ x2 (proof)
Known PowerEPowerE : ∀ x0 x1 . x1prim4 x0x1x0
Theorem V_E : ∀ x0 x1 . x0V_ x1∀ x2 : ο . (∀ x3 . x3x1x0V_ x3x2)x2 (proof)
Known In_indIn_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . x0 x1
Theorem V_Subq : ∀ x0 . x0V_ x0 (proof)
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Theorem V_Subq_2 : ∀ x0 x1 . x0V_ x1V_ x0V_ x1 (proof)
Theorem V_In : ∀ x0 x1 . x0V_ x1V_ x0V_ x1 (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Definition nInnIn := λ x0 x1 . not (x0x1)
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known FalseEFalseE : False∀ x0 : ο . x0
Theorem V_In_or_Subq : ∀ x0 x1 . or (x0V_ x1) (V_ x1V_ x0) (proof)
Theorem V_In_or_Subq_2 : ∀ x0 x1 . or (V_ x0V_ x1) (V_ x1V_ x0) (proof)
Definition famunion_closedfamunion_closed := λ x0 . ∀ x1 . x1x0∀ x2 : ι → ι . (∀ x3 . x3x1x2 x3x0)famunion x1 x2x0
Definition V_closed := λ x0 . ∀ x1 . x1x0V_ x1x0
Definition Union_closedUnion_closed := λ x0 . ∀ x1 . x1x0prim3 x1x0
Definition Repl_closedRepl_closed := λ x0 . ∀ x1 . x1x0∀ x2 : ι → ι . (∀ x3 . x3x1x2 x3x0)prim5 x1 x2x0
Theorem Union_Repl_famunion_closedUnion_Repl_famunion_closed : ∀ x0 . Union_closed x0Repl_closed x0famunion_closed x0 (proof)
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Param ZF_closedZF_closed : ιο
Definition Power_closedPower_closed := λ x0 . ∀ x1 . x1x0prim4 x1x0
Known ZF_closed_EZF_closed_E : ∀ x0 . ZF_closed x0∀ x1 : ο . (Union_closed x0Power_closed x0Repl_closed x0x1)x1
Theorem V_U_In : ∀ x0 . TransSet x0ZF_closed x0V_closed x0 (proof)
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)
Param SepSep : ι(ιο) → ι
Definition ordinalordinal := λ x0 . and (TransSet x0) (∀ x1 . x1x0TransSet x1)
Param invinv : ι(ιι) → ιι
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Known ordinal_Heredordinal_Hered : ∀ x0 . ordinal x0∀ x1 . x1x0ordinal x1
Known bij_invbij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2bij x1 x0 (inv x0 x2)
Known or3Eor3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2∀ x3 : ο . (x0x3)(x1x3)(x2x3)x3
Known ordinal_trichotomy_orordinal_trichotomy_or : ∀ x0 x1 . ordinal x0ordinal x1or (or (x0x1) (x0 = x1)) (x1x0)
Known SepE2SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x1 x2
Known pred_ext_2pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2x1 x2)(∀ x2 . x1 x2x0 x2)x0 = x1
Known Eps_i_exEps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Param ReplSepReplSep : ι(ιο) → (ιι) → ι
Known 9248b.. : ∀ x0 x1 . x1x0∀ x2 : ο . (∀ x3 . and (x3x0) (not (∀ x4 : ο . (∀ x5 . and (x5x0) (x5x3)x4)x4))x2)x2
Known ReplSepIReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3x0x1 x3x2 x3ReplSep x0 x1 x2
Known ReplSepE_impredReplSepE_impred : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3ReplSep x0 x1 x2∀ x4 : ο . (∀ x5 . x5x0x1 x5x3 = x2 x5x4)x4
Theorem TarskiA_bij_ord : ∀ x0 . TransSet x0ZF_closed x0∀ x1 . x1x0nIn x1 x0∀ x2 : ο . (∀ x3 : ι → ι . bij (Sep x0 ordinal) x1 x3x2)x2 (proof)
Known UnivOf_ZF_closedUnivOf_ZF_closed : ∀ x0 . ZF_closed (prim6 x0)
Known and4Iand4I : ∀ x0 x1 x2 x3 : ο . x0x1x2x3and (and (and x0 x1) x2) x3
Known UnivOf_InUnivOf_In : ∀ x0 . x0prim6 x0
Known UnivOf_TransSetUnivOf_TransSet : ∀ x0 . TransSet (prim6 x0)
Known Subq_refSubq_ref : ∀ x0 . x0x0
Known bij_compbij_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . bij x0 x1 x3bij x1 x2 x4bij x0 x2 (λ x5 . x4 (x3 x5))
Theorem TarskiA : ∀ x0 . ∀ x1 : ο . (∀ x2 . and (and (and (x0x2) (∀ x3 . x3x2∀ x4 . x4x3x4x2)) (∀ x3 . x3x2∀ x4 : ο . (∀ x5 . and (x5x2) (∀ x6 . x6x3x6x5)x4)x4)) (∀ x3 . x3x2or (∀ x4 : ο . (∀ x5 : ι → ι . bij x3 x2 x5x4)x4) (x3x2))x1)x1 (proof)

previous assets