Apply 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 with ∀ x0 : ι → ι → ο . wb (wnfc (λ x1 . x0 x1)) (∀ x1 . wnf (λ x2 . wcel (cv x1) (x0 x2))).

Assume H0: ∀ x0 : ι → ο . (∀ x1 x2 . x0 x2) ⟶ ∀ x1 x2 . x0 x2.

Assume H1: ∀ x0 : ι → ι → ο . ∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ (∀ x3 . x0 x1 x3) ⟶ ∀ x3 . wceq (cv x3) (cv x2) ⟶ x0 x3 x2.

Assume H2: ∀ x0 : ι → ο . ∀ x1 . wceq (cv x1) (cv x1) ⟶ (∀ x2 . x0 x2) ⟶ ∀ x2 . wceq (cv x2) (cv x2) ⟶ x0 x2.

Assume H3: ∀ x0 x1 x2 . wn (wceq (cv x2) (cv x0)) ⟶ wceq (cv x0) (cv x1) ⟶ ∀ x3 . wceq (cv x0) (cv x1).

Assume H4: ∀ x0 x1 . wn (wceq (cv x1) (cv x1)) ⟶ wceq (cv x1) (cv x0) ⟶ ∀ x2 . wceq (cv x2) (cv x0).

Assume H5: ∀ x0 : ι → ο . wb (weu (λ x1 . x0 x1)) (wex (λ x1 . ∀ x2 . wb (x0 x2) (wceq (cv x2) (cv x1)))).

Assume H6: ∀ x0 : ι → ο . wb (wmo (λ x1 . x0 x1)) (wex (λ x1 . x0 x1) ⟶ weu (λ x1 . x0 x1)).

Assume H7: ∀ x0 x1 . (∀ x2 . wb (wcel (cv x2) (cv x0)) (wcel (cv x2) (cv x1))) ⟶ wceq (cv x0) (cv x1).

Assume H8: ∀ x0 : ι → ο . ∀ x1 . wb (wcel (cv x1) (cab (λ x2 . x0 x2))) (wsb (λ x2 . x0 x2) x1).

Assume H9: ∀ x0 : ι → ο . ∀ x1 . wb (wcel (cv x1) (cab (λ x2 . x0 x2))) (wsb (λ x2 . x0 x2) x1).

Assume H10: ∀ 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))).

Assume H11: ∀ x0 x1 : ι → ο . wb (wcel x0 x1) (wex (λ x2 . wa (wceq (cv x2) x0) (wcel (cv x2) x1))).

Assume H12: ∀ x0 : ι → ι → ο . wb (wnfc (λ x1 . x0 x1)) (∀ x1 . wnf (λ x2 . wcel (cv x1) (x0 ...))).

...

■

Proofgold Proof