Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known In_ind^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 9248b.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (not (∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x5 ∈ x3) ⟶ x4) ⟶ x4)) ⟶ x2) ⟶ x2 (proof)
Param In_rec_i^In_rec_i : (ι → (ι → ι) → ι) → ι → ι
Param famunion^famunion : ι → (ι → ι) → ι
Definition V_ := In_rec_i (λ x0 . λ x1 : ι → ι . famunion x0 (λ x2 . prim4 (x1 x2)))
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known In_rec_i_eq^In_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i x0 x1 = x0 x1 (In_rec_i x0)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known famunionE^famunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 ∈ x1 x4) ⟶ x3) ⟶ x3
Known famunionI^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ x0 ⟶ x3 ∈ x1 x2 ⟶ x3 ∈ famunion x0 x1
Theorem V_eq : ∀ x0 . V_ x0 = famunion x0 (λ x2 . prim4 (V_ x2)) (proof)
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Theorem V_I : ∀ x0 x1 x2 . x1 ∈ x2 ⟶ x0 ⊆ V_ x1 ⟶ x0 ∈ V_ x2 (proof)
Known PowerE^PowerE : ∀ x0 x1 . x1 ∈ prim4 x0 ⟶ x1 ⊆ x0
Theorem V_E : ∀ x0 x1 . x0 ∈ V_ x1 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ V_ x3 ⟶ x2) ⟶ x2 (proof)
Theorem V_Subq : ∀ x0 . x0 ⊆ V_ x0 (proof)
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Theorem V_Subq_2 : ∀ x0 x1 . x0 ⊆ V_ x1 ⟶ V_ x0 ⊆ V_ x1 (proof)
Theorem V_In : ∀ x0 x1 . x0 ∈ V_ x1 ⟶ V_ x0 ∈ V_ x1 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem V_In_or_Subq : ∀ x0 x1 . or (x0 ∈ V_ x1) (V_ x1 ⊆ V_ x0) (proof)
Theorem V_In_or_Subq_2 : ∀ x0 x1 . or (V_ x0 ∈ V_ x1) (V_ x1 ⊆ V_ x0) (proof)
Definition V_closed := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ V_ x1 ∈ x0
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Param ZF_closed^ZF_closed : ι → ο
Param Union_closed^Union_closed : ι → ο
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
Known ZF_closed_E^ZF_closed_E : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 : ο . (Union_closed x0 ⟶ Power_closed x0 ⟶ Repl_closed x0 ⟶ x1) ⟶ x1
Definition famunion_closed^{famunion_closed} := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0) ⟶ famunion x1 x2 ∈ x0
Known Union_Repl_famunion_closed^{Union_Repl_famunion_closed} : ∀ x0 . Union_closed x0 ⟶ Repl_closed x0 ⟶ famunion_closed x0
Theorem V_U_In : ∀ x0 . TransSet x0 ⟶ ZF_closed x0 ⟶ V_closed x0 (proof)
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)
Param Sep^Sep : ι → (ι → ο) → ι
Definition ordinal^ordinal := λ x0 . and (TransSet x0) (∀ x1 . x1 ∈ x0 ⟶ TransSet x1)
Param inv^inv : ι → (ι → ι) → ι → ι
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Known ordinal_Hered^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordinal x1
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known bij_inv^bij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ bij x1 x0 (inv x0 x2)
Known or3E^or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Known ordinal_trichotomy_or^{ordinal_trichotomy_or} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (x0 ∈ x1) (x0 = x1)) (x1 ∈ x0)
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Param ReplSep^ReplSep : ι → (ι → ο) → (ι → ι) → ι
Known ReplSepE_impred^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ ReplSep x0 x1 x2 ⟶ ∀ x4 : ο . (∀ x5 . x5 ∈ x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Known ReplSepI^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⟶ x2 x3 ∈ ReplSep x0 x1 x2
Known pred_ext_2^pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Theorem TarskiA_bij_ord : ∀ x0 . TransSet x0 ⟶ ZF_closed x0 ⟶ ∀ x1 . x1 ⊆ x0 ⟶ nIn x1 x0 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . bij (Sep x0 ordinal) x1 x3 ⟶ x2) ⟶ x2 (proof)
Known UnivOf_ZF_closed^{UnivOf_ZF_closed} : ∀ x0 . ZF_closed (prim6 x0)
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Known UnivOf_In^UnivOf_In : ∀ x0 . x0 ∈ prim6 x0
Known UnivOf_TransSet^{UnivOf_TransSet} : ∀ x0 . TransSet (prim6 x0)
Known bij_comp^bij_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . bij x0 x1 x3 ⟶ bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5))
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Theorem TarskiA : ∀ x0 . ∀ x1 : ο . (∀ x2 . and (and (and (x0 ∈ x2) (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ⊆ x3 ⟶ x4 ∈ x2)) (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x2) (∀ x6 . x6 ⊆ x3 ⟶ x6 ∈ x5) ⟶ x4) ⟶ x4)) (∀ x3 . x3 ⊆ x2 ⟶ or (∀ x4 : ο . (∀ x5 : ι → ι . bij x3 x2 x5 ⟶ x4) ⟶ x4) (x3 ∈ x2)) ⟶ x1) ⟶ x1 (proof)
Theorem 24558.. : ∀ x0 . nIn x0 (V_ x0) (proof)
Theorem 6fa7f.. : ∀ x0 . V_ (V_ x0) = V_ x0 (proof)
Theorem 26f65.. : ∀ x0 x1 . x0 ∈ x1 ⟶ V_ x0 ∈ V_ x1 (proof)
Theorem ebb40.. : ∀ x0 . TransSet (V_ x0) (proof)
Param ordsucc^ordsucc : ι → ι
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 31c56.. : ∀ x0 x1 . x1 ⊆ V_ x0 ⟶ x1 ∈ V_ (ordsucc x0) (proof)
Definition 9d271.. := λ x0 . Sep (V_ x0) ordinal
Theorem 6092a.. : ∀ x0 . ordinal (9d271.. x0) (proof)
Known Sep_Subq^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ⊆ x0
Theorem e7373.. : ∀ x0 x1 . x0 ∈ x1 ⟶ 9d271.. x0 ∈ 9d271.. x1 (proof)
Theorem 5bd9b.. : ∀ x0 . V_ (9d271.. x0) = V_ x0 (proof)
Theorem 8b439.. : ∀ x0 . x0 ⊆ V_ (9d271.. x0) (proof)
Param Inj1^Inj1 : ι → ι
Known Inj1E^Inj1E : ∀ x0 x1 . x1 ∈ Inj1 x0 ⟶ or (x1 = 0) (∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (x1 = Inj1 x3) ⟶ x2) ⟶ x2)
Known Subq_Empty^Subq_Empty : ∀ x0 . 0 ⊆ x0
Known ordinal_ordsucc_In^{ordinal_ordsucc_In} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Theorem c6442.. : ∀ x0 . Inj1 x0 ⊆ V_ (ordsucc (9d271.. x0)) (proof)
Param Inj0^Inj0 : ι → ι
Known Inj0E^Inj0E : ∀ x0 x1 . x1 ∈ Inj0 x0 ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (x1 = Inj1 x3) ⟶ x2) ⟶ x2
Theorem a07a1.. : ∀ x0 . Inj0 x0 ⊆ V_ (ordsucc (9d271.. x0)) (proof)
Param setsum^setsum : ι → ι → ι
Param binunion^binunion : ι → ι → ι
Known setsum_Inj_inv^{setsum_Inj_inv} : ∀ x0 x1 x2 . x2 ∈ setsum x0 x1 ⟶ or (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = Inj0 x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (x2 = Inj1 x4) ⟶ x3) ⟶ x3)
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known ordinal_binunion^{ordinal_binunion} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (binunion x0 x1)
Theorem 4cbae.. : ∀ x0 x1 . setsum x0 x1 ⊆ V_ (ordsucc (binunion (9d271.. x0) (9d271.. x1))) (proof)
Param lam^Sigma : ι → (ι → ι) → ι
Known lamE^lamE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x1 x4) (x2 = setsum x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known ordinal_linear^{ordinal_linear} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ⊆ x1) (x1 ⊆ x0)
Known Subq_binunion_eq^{Subq_binunion_eq} : ∀ x0 x1 . x0 ⊆ x1 = (binunion x0 x1 = x1)
Known binunion_com^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Theorem f95aa.. : ∀ x0 . ∀ x1 : ι → ι . lam x0 x1 ⊆ V_ (ordsucc (binunion (ordsucc (9d271.. x0)) (famunion x0 (λ x2 . ordsucc (9d271.. (x1 x2)))))) (proof)
Known ordinal_In_Or_Subq^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ∈ x1) (x1 ⊆ x0)
Known ordinal_ordsucc^{ordinal_ordsucc} : ∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0)
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Theorem f0633.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ x0 ⊆ x1 ⟶ ordsucc x0 ⊆ ordsucc x1 (proof)
Param Pi^Pi : ι → (ι → ι) → ι
Param ap^ap : ι → ι → ι
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Known binunion_Subq_1^{binunion_Subq_1} : ∀ x0 x1 . x0 ⊆ binunion x0 x1
Known famunionE_impred^{famunionE_impred} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 ∈ x1 x4 ⟶ x3) ⟶ x3
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known binunion_Subq_2^{binunion_Subq_2} : ∀ x0 x1 . x1 ⊆ binunion x0 x1
Known ordinal_famunion^{ordinal_famunion} : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ordinal (x1 x2)) ⟶ ordinal (famunion x0 x1)
Theorem c0b6d.. : ∀ x0 . ∀ x1 : ι → ι . Pi x0 x1 ⊆ V_ (ordsucc (ordsucc (binunion (ordsucc (9d271.. x0)) (famunion x0 (λ x2 . ordsucc (9d271.. (x1 x2))))))) (proof)