Apply df_ec__df_qs__df_map__df_pm__df_ixp__df_en__df_dom__df_sdom__df_fin__df_fsupp__df_fi__df_sup__df_inf__df_oi__df_har__df_wdom__ax_reg__ax_inf with ∀ x0 x1 x2 : ι → ο . wceq (csup x0 x1 x2) (cuni (crab (λ x3 . wa (wral (λ x4 . wn (wbr (cv x3) (cv x4) x2)) (λ x4 . x0)) (wral (λ x4 . wbr (cv x4) (cv x3) x2 ⟶ wrex (λ x5 . wbr (cv x4) (cv x5) x2) (λ x5 . x0)) (λ x4 . x1))) (λ x3 . x1))).

Assume H0: ∀ x0 x1 : ι → ο . wceq (cec x0 x1) (cima x1 (csn x0)).

Assume H1: ∀ x0 x1 : ι → ο . wceq (cqs x0 x1) (cab (λ x2 . wrex (λ x3 . wceq (cv x2) (cec (cv x3) x1)) (λ x3 . x0))).

Assume H2: wceq cmap (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cab (λ x2 . wf (cv x1) (cv x0) (cv x2)))).

Assume H3: wceq cpm (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wfun (cv x2)) (λ x2 . cpw (cxp (cv x1) (cv x0))))).

Assume H4: ∀ x0 x1 : ι → ι → ο . wceq (cixp (λ x2 . x0 x2) (λ x2 . x1 x2)) (cab (λ x2 . wa (wfn (cv x2) (cab (λ x3 . wcel (cv x3) (x0 x3)))) (wral (λ x3 . wcel (cfv (cv x3) (cv x2)) (x1 x3)) (λ x3 . x0 x3)))).

Assume H5: wceq cen (copab (λ x0 x1 . wex (λ x2 . wf1o (cv x0) (cv x1) (cv x2)))).

Assume H6: wceq cdom (copab (λ x0 x1 . wex (λ x2 . wf1 (cv x0) (cv x1) (cv x2)))).

Assume H7: wceq csdm (cdif cdom cen).

Assume H8: wceq cfn (cab (λ x0 . wrex (λ x1 . wbr (cv x0) (cv x1) cen) (λ x1 . com))).

Assume H9: wceq cfsupp (copab (λ x0 x1 . wa (wfun (cv x0)) (wcel (co (cv x0) (cv x1) csupp) cfn))).

Assume H10: wceq cfi (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wrex (λ x2 . wceq (cv x1) (cint (cv x2))) (λ x2 . cin (cpw (cv x0)) cfn)))).

Assume H11: ∀ x0 x1 x2 : ι → ο . wceq (csup x0 x1 x2) (cuni (crab (λ x3 . wa (wral (λ x4 . wn (wbr (cv x3) (cv x4) x2)) (λ x4 . x0)) ...) ...)).

...

■

Proofgold Proof