Proofgold Address

Known ax_11_b__ax_12__ax_12_b__ax_13__ax_13_b__df_eu__df_mo__ax_ext__df_clab__df_clab_b__df_cleq__df_clel__df_nfc__df_ne__df_nel__df_ral__df_rex__df_reu : ∀ x0 : ο . ((∀ x1 : ι → ο . (∀ x2 x3 . x1 x3) ⟶ ∀ x2 x3 . x1 x3) ⟶ (∀ x1 : ι → ι → ο . ∀ x2 x3 . wceq (cv x2) (cv x3) ⟶ (∀ x4 . x1 x2 x4) ⟶ ∀ x4 . wceq (cv x4) (cv x3) ⟶ x1 x4 x3) ⟶ (∀ x1 : ι → ο . ∀ x2 . wceq (cv x2) (cv x2) ⟶ (∀ x3 . x1 x3) ⟶ ∀ x3 . wceq (cv x3) (cv x3) ⟶ x1 x3) ⟶ (∀ x1 x2 x3 . wn (wceq (cv x3) (cv x1)) ⟶ wceq (cv x1) (cv x2) ⟶ ∀ x4 . wceq (cv x1) (cv x2)) ⟶ (∀ x1 x2 . wn (wceq (cv x2) (cv x2)) ⟶ wceq (cv x2) (cv x1) ⟶ ∀ x3 . wceq (cv x3) (cv x1)) ⟶ (∀ x1 : ι → ο . wb (weu x1) (wex (λ x2 . ∀ x3 . wb (x1 x3) (wceq (cv x3) (cv x2))))) ⟶ (∀ x1 : ι → ο . wb (wmo x1) (wex x1 ⟶ weu x1)) ⟶ (∀ x1 x2 . (∀ x3 . wb (wcel (cv x3) (cv x1)) (wcel (cv x3) (cv x2))) ⟶ wceq (cv x1) (cv x2)) ⟶ (∀ x1 : ι → ο . ∀ x2 . wb (wcel (cv x2) (cab x1)) (wsb x1 x2)) ⟶ (∀ x1 : ι → ο . ∀ x2 . wb (wcel (cv x2) (cab x1)) (wsb x1 x2)) ⟶ (∀ x1 x2 : ι → ι → ι → ο . (∀ x3 x4 . (∀ x5 . wb (wcel (cv x5) (cv x3)) (wcel (cv x5) (cv x4))) ⟶ wceq (cv x3) (cv x4)) ⟶ ∀ x3 x4 . wb (wceq (x1 x3 x4) (x2 x3 x4)) (∀ x5 . wb (wcel (cv x5) (x1 x3 x4)) (wcel (cv x5) (x2 x3 x4)))) ⟶ (∀ x1 x2 : ι → ο . wb (wcel x1 x2) (wex (λ x3 . wa (wceq (cv x3) x1) (wcel (cv x3) x2)))) ⟶ (∀ x1 : ι → ι → ο . wb (wnfc x1) (∀ x2 . wnf (λ x3 . wcel (cv x2) (x1 x3)))) ⟶ (∀ x1 x2 : ι → ο . wb (wne x1 x2) (wn (wceq x1 x2))) ⟶ (∀ x1 x2 : ι → ο . wb (wnel x1 x2) (wn (wcel x1 x2))) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wb (wral x1 x2) (∀ x3 . wcel (cv x3) (x2 x3) ⟶ x1 x3)) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wb (wrex x1 x2) (wex (λ x3 . wa (wcel (cv x3) (x2 x3)) (x1 x3)))) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wb (wreu x1 x2) (weu (λ x3 . wa (wcel (cv x3) (x2 x3)) (x1 x3)))) ⟶ x0) ⟶ x0
Theorem ax_11_b : ∀ x0 : ι → ο . (∀ x1 x2 . x0 x2) ⟶ ∀ x1 x2 . x0 x2 (proof)
Theorem ax_11d : ∀ x0 : ι → ι → ο . ∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ (∀ x3 . x0 x1 x3) ⟶ ∀ x3 . wceq (cv x3) (cv x2) ⟶ x0 x3 x2 (proof)
Theorem ax_12_b : ∀ x0 : ι → ο . ∀ x1 . wceq (cv x1) (cv x1) ⟶ (∀ x2 . x0 x2) ⟶ ∀ x2 . wceq (cv x2) (cv x2) ⟶ x0 x2 (proof)
Theorem ax_13 : ∀ x0 x1 x2 . wn (wceq (cv x2) (cv x0)) ⟶ wceq (cv x0) (cv x1) ⟶ ∀ x3 . wceq (cv x0) (cv x1) (proof)
Theorem ax_13_b : ∀ x0 x1 . wn (wceq (cv x1) (cv x1)) ⟶ wceq (cv x1) (cv x0) ⟶ ∀ x2 . wceq (cv x2) (cv x0) (proof)
Theorem df_eu : ∀ x0 : ι → ο . wb (weu x0) (wex (λ x1 . ∀ x2 . wb (x0 x2) (wceq (cv x2) (cv x1)))) (proof)
Theorem df_mo : ∀ x0 : ι → ο . wb (wmo x0) (wex x0 ⟶ weu x0) (proof)
Theorem ax_ext : ∀ x0 x1 . (∀ x2 . wb (wcel (cv x2) (cv x0)) (wcel (cv x2) (cv x1))) ⟶ wceq (cv x0) (cv x1) (proof)
Theorem df_clab_b : ∀ x0 : ι → ο . ∀ x1 . wb (wcel (cv x1) (cab x0)) (wsb x0 x1) (proof)
Theorem df_clab_b : ∀ x0 : ι → ο . ∀ x1 . wb (wcel (cv x1) (cab x0)) (wsb x0 x1) (proof)
Theorem df_cleq : ∀ x0 x1 : ι → ι → ι → ο . (∀ x2 x3 . (∀ x4 . wb (wcel (cv x4) (cv x2)) (wcel (cv x4) (cv x3))) ⟶ wceq (cv x2) (cv x3)) ⟶ ∀ x2 x3 . wb (wceq (x0 x2 x3) (x1 x2 x3)) (∀ x4 . wb (wcel (cv x4) (x0 x2 x3)) (wcel (cv x4) (x1 x2 x3))) (proof)
Theorem df_clel : ∀ x0 x1 : ι → ο . wb (wcel x0 x1) (wex (λ x2 . wa (wceq (cv x2) x0) (wcel (cv x2) x1))) (proof)
Theorem df_nfc : ∀ x0 : ι → ι → ο . wb (wnfc x0) (∀ x1 . wnf (λ x2 . wcel (cv x1) (x0 x2))) (proof)
Theorem df_ne : ∀ x0 x1 : ι → ο . wb (wne x0 x1) (wn (wceq x0 x1)) (proof)
Theorem df_nel : ∀ x0 x1 : ι → ο . wb (wnel x0 x1) (wn (wcel x0 x1)) (proof)
Theorem df_ral : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wb (wral x0 x1) (∀ x2 . wcel (cv x2) (x1 x2) ⟶ x0 x2) (proof)
Theorem df_rex : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wb (wrex x0 x1) (wex (λ x2 . wa (wcel (cv x2) (x1 x2)) (x0 x2))) (proof)
Theorem df_reu : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wb (wreu x0 x1) (weu (λ x2 . wa (wcel (cv x2) (x1 x2)) (x0 x2))) (proof)