Apply df_fr__df_se__df_we__df_xp__df_rel__df_cnv__df_co__df_dm__df_rn__df_res__df_ima__df_pred__df_ord__df_on__df_lim__df_suc__df_iota__df_fun with ∀ x0 : ι → ο . wb (wfun x0) (wa (wrel x0) (wss (ccom x0 (ccnv x0)) cid)).

Assume H0: ∀ x0 x1 : ι → ο . wb (wfr x0 x1) (∀ x2 . wa (wss (cv x2) x0) (wne (cv x2) c0) ⟶ wrex (λ x3 . wral (λ x4 . wn (wbr (cv x4) (cv x3) x1)) (λ x4 . cv x2)) (λ x3 . cv x2)).

Assume H1: ∀ x0 x1 : ι → ο . wb (wse x0 x1) (wral (λ x2 . wcel (crab (λ x3 . wbr (cv x3) (cv x2) x1) (λ x3 . x0)) cvv) (λ x2 . x0)).

Assume H2: ∀ x0 x1 : ι → ο . wb (wwe x0 x1) (wa (wfr x0 x1) (wor x0 x1)).

Assume H3: ∀ x0 x1 : ι → ο . wceq (cxp x0 x1) (copab (λ x2 x3 . wa (wcel (cv x2) x0) (wcel (cv x3) x1))).

Assume H4: ∀ x0 : ι → ο . wb (wrel x0) (wss x0 (cxp cvv cvv)).

Assume H5: ∀ x0 : ι → ο . wceq (ccnv x0) (copab (λ x1 x2 . wbr (cv x2) (cv x1) x0)).

Assume H6: ∀ x0 x1 : ι → ο . wceq (ccom x0 x1) (copab (λ x2 x3 . wex (λ x4 . wa (wbr (cv x2) (cv x4) x1) (wbr (cv x4) (cv x3) x0)))).

Assume H7: ∀ x0 : ι → ο . wceq (cdm x0) (cab (λ x1 . wex (λ x2 . wbr (cv x1) (cv x2) x0))).

Assume H8: ∀ x0 : ι → ο . wceq (crn x0) (cdm (ccnv x0)).

Assume H9: ∀ x0 x1 : ι → ο . wceq (cres x0 x1) (cin x0 (cxp x1 cvv)).

Assume H10: ∀ x0 x1 : ι → ο . wceq (cima x0 x1) (crn (cres x0 x1)).

Assume H11: ∀ x0 x1 x2 : ι → ο . wceq (cpred x0 x1 x2) (cin x0 (cima (ccnv x1) (csn x2))).

Assume H12: ∀ x0 : ι → ο . wb (word x0) (wa (wtr x0) (wwe x0 cep)).

Assume H13: wceq con0 (cab (λ x0 . word (cv x0))).

Assume H14: ∀ x0 : ι → ο . wb (wlim x0) (w3a (word x0) (wne x0 c0) (wceq x0 (cuni x0))).

Assume H15: ∀ x0 : ι → ο . wceq (csuc x0) (cun x0 (csn x0)).

Assume H16: ∀ x0 : ι → ο . wceq (cio (λ x1 . x0 x1)) (cuni (cab (λ x1 . wceq (cab (λ x2 . x0 x2)) ...))).

...

■

Proofgold Proof