Proofgold Asset

Prim 0/2b9fe.. : (ι → ο) → ι
Axiom Eps_i_ax^Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Def False^False : ο := ∀ x0 : ο . x0
Def not^not : ο → ο := λ x0 : ο . x0 ⟶ False
Def and^and : ο → ο → ο := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Def or^or : ο → ο → ο := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Def iff^iff : ο → ο → ο := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Axiom prop_ext^prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Prim 1/5341a.. : ι → ι → ο
Def Subq^Subq : ι → ι → ο := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Axiom set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Axiom In_ind^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Prim 2/dee93.. : ι
Axiom EmptyAx^EmptyAx : not (∀ x0 : ο . (∀ x1 . x1 ∈ 0 ⟶ x0) ⟶ x0)
Prim 3/e1447.. : ι → ι
Axiom UnionEq^UnionEq : ∀ x0 x1 . iff (x1 ∈ prim3 x0) (∀ x2 : ο . (∀ x3 . and (x1 ∈ x3) (x3 ∈ x0) ⟶ x2) ⟶ x2)
Prim 4/0a620.. : ι → ι
Axiom PowerEq^PowerEq : ∀ x0 x1 . iff (x1 ∈ prim4 x0) (x1 ⊆ x0)
Prim 5/8641c.. : ι → (ι → ι) → ι
Axiom ReplEq^ReplEq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (x2 ∈ prim5 x0 x1) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = x1 x4) ⟶ x3) ⟶ x3)
Def TransSet^TransSet : ι → ο := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Def Union_closed^Union_closed : ι → ο := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ prim3 x1 ∈ x0
Def Power_closed^Power_closed : ι → ο := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ prim4 x1 ∈ x0
Def Repl_closed^Repl_closed : ι → ο := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0) ⟶ prim5 x1 x2 ∈ x0
Def ZF_closed^ZF_closed : ι → ο := λ x0 . and (and (Union_closed x0) (Power_closed x0)) (Repl_closed x0)
Prim 6/1ae92.. : ι → ι
Axiom UnivOf_In^UnivOf_In : ∀ x0 . x0 ∈ prim6 x0
Axiom UnivOf_TransSet^{UnivOf_TransSet} : ∀ x0 . TransSet (prim6 x0)
Axiom UnivOf_ZF_closed^{UnivOf_ZF_closed} : ∀ x0 . ZF_closed (prim6 x0)
Axiom UnivOf_Min^UnivOf_Min : ∀ x0 x1 . x0 ∈ x1 ⟶ TransSet x1 ⟶ ZF_closed x1 ⟶ prim6 x0 ⊆ x1