Proofgold Address

Param In_rec_i^In_rec_i : (ι → (ι → ι) → ι) → ι → ι
Definition famunion^famunion := λ x0 . λ x1 : ι → ι . prim3 (prim5 x0 x1)
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
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
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)
Known In_ind^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
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
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and 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 famunion_closed^{famunion_closed} := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0) ⟶ famunion x1 x2 ∈ x0
Definition V_closed := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ V_ x1 ∈ x0
Definition Union_closed^Union_closed := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ prim3 x1 ∈ x0
Definition Repl_closed^Repl_closed := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0) ⟶ prim5 x1 x2 ∈ x0
Theorem Union_Repl_famunion_closed^{Union_Repl_famunion_closed} : ∀ x0 . Union_closed x0 ⟶ Repl_closed x0 ⟶ famunion_closed x0 (proof)
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Param ZF_closed^ZF_closed : ι → ο
Definition Power_closed^Power_closed := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ prim4 x1 ∈ x0
Known ZF_closed_E^ZF_closed_E : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 : ο . (Union_closed x0 ⟶ Power_closed x0 ⟶ Repl_closed x0 ⟶ x1) ⟶ x1
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 ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
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 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 pred_ext_2^pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Param ReplSep^ReplSep : ι → (ι → ο) → (ι → ι) → ι
Known 9248b.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (not (∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x5 ∈ x3) ⟶ x4) ⟶ x4)) ⟶ x2) ⟶ x2
Known ReplSepI^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⟶ x2 x3 ∈ ReplSep x0 x1 x2
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
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 Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ 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))
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)