Proofgold Address

Param 1ce4f..^incl_0_1 : ι → ι → ο
Definition 00f04..^down_1_0 := λ x0 : ι → ο . Eps_i (λ x1 . 1ce4f.. x1 = x0)
Param Descr_Vo1^Descr_Vo1 : ((ι → ο) → ο) → ι → ο
Param 407b5..^incl_1_2 : (ι → ο) → (ι → ο) → ο
Definition 3e5e9..^down_2_1 := λ x0 : (ι → ο) → ο . Descr_Vo1 (λ x1 : ι → ο . 407b5.. x1 = x0)
Param Descr_Vo2^Descr_Vo2 : (((ι → ο) → ο) → ο) → (ι → ο) → ο
Param 3a6d0..^In_2 : ((ι → ο) → ο) → ((ι → ο) → ο) → ο
Definition a4b00..^incl_2_3 := λ x0 x1 : (ι → ο) → ο . 3a6d0.. x1 x0
Definition d94e6..^down_3_2 := λ x0 : ((ι → ο) → ο) → ο . Descr_Vo2 (λ x1 : (ι → ο) → ο . a4b00.. x1 = x0)
Param Descr_Vo3^Descr_Vo3 : ((((ι → ο) → ο) → ο) → ο) → ((ι → ο) → ο) → ο
Param e6217..^In_3 : (((ι → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο
Definition a327b..^incl_3_4 := λ x0 x1 : ((ι → ο) → ο) → ο . e6217.. x1 x0
Definition dba53..^down_4_3 := λ x0 : (((ι → ο) → ο) → ο) → ο . Descr_Vo3 (λ x1 : ((ι → ο) → ο) → ο . a327b.. x1 = x0)
Known c0781..^incl_0_1_inj : ∀ x0 x1 . 1ce4f.. x0 = 1ce4f.. x1 ⟶ x0 = x1
Known 4cb75..^Eps_i_R : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (Eps_i x0)
Theorem 9056c..^{down_1_0_incl_0_1} : ∀ x0 . 00f04.. (1ce4f.. x0) = x0 (proof)
Known 94a3d..^incl_1_2_inj : ∀ x0 x1 : ι → ο . 407b5.. x0 = 407b5.. x1 ⟶ x0 = x1
Known Descr_Vo1_prop^{Descr_Vo1_prop} : ∀ x0 : (ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo1 x0)
Theorem 966b6..^{down_2_1_incl_1_2} : ∀ x0 : ι → ο . 3e5e9.. (407b5.. x0) = x0 (proof)
Known ea98f..^incl_2_3_inj : ∀ x0 x1 : (ι → ο) → ο . a4b00.. x0 = a4b00.. x1 ⟶ x0 = x1
Known Descr_Vo2_prop^{Descr_Vo2_prop} : ∀ x0 : ((ι → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : (ι → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : (ι → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo2 x0)
Theorem 34c81..^{down_3_2_incl_2_3} : ∀ x0 : (ι → ο) → ο . d94e6.. (a4b00.. x0) = x0 (proof)
Known 79850..^incl_3_4_inj : ∀ x0 x1 : ((ι → ο) → ο) → ο . a327b.. x0 = a327b.. x1 ⟶ x0 = x1
Known Descr_Vo3_prop^{Descr_Vo3_prop} : ∀ x0 : (((ι → ο) → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : ((ι → ο) → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ((ι → ο) → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo3 x0)
Theorem ef47b..^{down_4_3_incl_3_4} : ∀ x0 : ((ι → ο) → ο) → ο . dba53.. (a327b.. x0) = x0 (proof)
Definition fb56c..^AC_1 := ∀ x0 : ο . (∀ x1 : ((ι → ο) → ο) → ι → ο . (∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ο . x2 x3 ⟶ x2 (x1 x2)) ⟶ x0) ⟶ x0
Definition 2f0a8..^AC_2 := ∀ x0 : ο . (∀ x1 : (((ι → ο) → ο) → ο) → (ι → ο) → ο . (∀ x2 : ((ι → ο) → ο) → ο . ∀ x3 : (ι → ο) → ο . x2 x3 ⟶ x2 (x1 x2)) ⟶ x0) ⟶ x0
Definition cfa90..^AC_3 := ∀ x0 : ο . (∀ x1 : ((((ι → ο) → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x2 : (((ι → ο) → ο) → ο) → ο . ∀ x3 : ((ι → ο) → ο) → ο . x2 x3 ⟶ x2 (x1 x2)) ⟶ x0) ⟶ x0
Known af1a5..^In_3_E : ∀ x0 x1 : ((ι → ο) → ο) → ο . e6217.. x0 x1 ⟶ ∀ x2 : (((ι → ο) → ο) → ο) → ο . (∀ x3 : (ι → ο) → ο . x1 x3 ⟶ x2 (a4b00.. x3)) ⟶ x2 x0
Known 7abdf..^In_3_I : ∀ x0 : (ι → ο) → ο . ∀ x1 : ((ι → ο) → ο) → ο . x1 x0 ⟶ e6217.. (a4b00.. x0) x1
Theorem 03bab..^{AC_3_imp_AC_2} : cfa90.. ⟶ 2f0a8.. (proof)
Known 724a1..^In_2_E : ∀ x0 x1 : (ι → ο) → ο . 3a6d0.. x0 x1 ⟶ ∀ x2 : ((ι → ο) → ο) → ο . (∀ x3 : ι → ο . x1 x3 ⟶ x2 (407b5.. x3)) ⟶ x2 x0
Known 5b9f0..^In_2_I : ∀ x0 : ι → ο . ∀ x1 : (ι → ο) → ο . x1 x0 ⟶ 3a6d0.. (407b5.. x0) x1
Theorem 5fbe6..^{AC_2_imp_AC_1} : 2f0a8.. ⟶ fb56c.. (proof)
Theorem 99a65..^Skolem_0 : ∀ x0 : ι → ι → ο . (∀ x1 . ∀ x2 : ο . (∀ x3 . x0 x1 x3 ⟶ x2) ⟶ x2) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι . (∀ x3 . x0 x3 (x2 x3)) ⟶ x1) ⟶ x1 (proof)
Theorem 3c207..^Skolem_0_bdd : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . In x2 x0 ⟶ ∀ x3 : ο . (∀ x4 . x1 x2 x4 ⟶ x3) ⟶ x3) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 . In x4 x0 ⟶ x1 x4 (x3 x4)) ⟶ x2) ⟶ x2 (proof)
Theorem 1b7fa..^Skolem_1 : fb56c.. ⟶ ∀ x0 : (ι → ο) → (ι → ο) → ο . (∀ x1 : ι → ο . ∀ x2 : ο . (∀ x3 : ι → ο . x0 x1 x3 ⟶ x2) ⟶ x2) ⟶ ∀ x1 : ο . (∀ x2 : (ι → ο) → ι → ο . (∀ x3 : ι → ο . x0 x3 (x2 x3)) ⟶ x1) ⟶ x1 (proof)
Param d97e3..^In_1 : (ι → ο) → (ι → ο) → ο
Theorem 3a35b..^Skolem_1_bdd : fb56c.. ⟶ ∀ x0 : ι → ο . ∀ x1 : (ι → ο) → (ι → ο) → ο . (∀ x2 : ι → ο . d97e3.. x2 x0 ⟶ ∀ x3 : ο . (∀ x4 : ι → ο . x1 x2 x4 ⟶ x3) ⟶ x3) ⟶ ∀ x2 : ο . (∀ x3 : (ι → ο) → ι → ο . (∀ x4 : ι → ο . d97e3.. x4 x0 ⟶ x1 x4 (x3 x4)) ⟶ x2) ⟶ x2 (proof)
Theorem c57b9..^Skolem_2 : 2f0a8.. ⟶ ∀ x0 : ((ι → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 : (ι → ο) → ο . ∀ x2 : ο . (∀ x3 : (ι → ο) → ο . x0 x1 x3 ⟶ x2) ⟶ x2) ⟶ ∀ x1 : ο . (∀ x2 : ((ι → ο) → ο) → (ι → ο) → ο . (∀ x3 : (ι → ο) → ο . x0 x3 (x2 x3)) ⟶ x1) ⟶ x1 (proof)
Theorem aa5c0..^Skolem_2_bdd : 2f0a8.. ⟶ ∀ x0 : (ι → ο) → ο . ∀ x1 : ((ι → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x2 : (ι → ο) → ο . 3a6d0.. x2 x0 ⟶ ∀ x3 : ο . (∀ x4 : (ι → ο) → ο . x1 x2 x4 ⟶ x3) ⟶ x3) ⟶ ∀ x2 : ο . (∀ x3 : ((ι → ο) → ο) → (ι → ο) → ο . (∀ x4 : (ι → ο) → ο . 3a6d0.. x4 x0 ⟶ x1 x4 (x3 x4)) ⟶ x2) ⟶ x2 (proof)
Theorem 42514..^Skolem_3 : cfa90.. ⟶ ∀ x0 : (((ι → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 : ((ι → ο) → ο) → ο . ∀ x2 : ο . (∀ x3 : ((ι → ο) → ο) → ο . x0 x1 x3 ⟶ x2) ⟶ x2) ⟶ ∀ x1 : ο . (∀ x2 : (((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x3 : ((ι → ο) → ο) → ο . x0 x3 (x2 x3)) ⟶ x1) ⟶ x1 (proof)
Theorem 7e268..^Skolem_3_bdd : cfa90.. ⟶ ∀ x0 : ((ι → ο) → ο) → ο . ∀ x1 : (((ι → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x2 : ((ι → ο) → ο) → ο . e6217.. x2 x0 ⟶ ∀ x3 : ο . (∀ x4 : ((ι → ο) → ο) → ο . x1 x2 x4 ⟶ x3) ⟶ x3) ⟶ ∀ x2 : ο . (∀ x3 : (((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x4 : ((ι → ο) → ο) → ο . e6217.. x4 x0 ⟶ x1 x4 (x3 x4)) ⟶ x2) ⟶ x2 (proof)