Proofgold Address

Known df_bj_rrvec__df_tau__df_finxp__ax_luk1__ax_luk2__ax_luk3__ax_wl_13v__ax_wl_11v__ax_wl_8cl__df_wl_clelv2__df_totbnd__df_bnd__df_ismty__df_rrn__df_ass__df_exid__df_mgmOLD__df_sgrOLD : ∀ x0 : ο . (wceq crrvec (crab (λ x1 . wceq (cfv (cv x1) csca) crefld) (λ x1 . clvec)) ⟶ wceq ctau (cinf (cin crp (cima (ccnv ccos) (csn c1))) cr clt) ⟶ (∀ x1 x2 : ι → ο . wceq (cfinxp x1 x2) (cab (λ x3 . wa (wcel x2 com) (wceq c0 (cfv x2 (crdg (cmpt2 (λ x4 x5 . com) (λ x4 x5 . cvv) (λ x4 x5 . cif (wa (wceq (cv x4) c1o) (wcel (cv x5) x1)) c0 (cif (wcel (cv x5) (cxp cvv x1)) (cop (cuni (cv x4)) (cfv (cv x5) c1st)) (cop (cv x4) (cv x5))))) (cop x2 (cv x3)))))))) ⟶ (∀ x1 x2 x3 : ο . (x1 ⟶ x2) ⟶ (x2 ⟶ x3) ⟶ x1 ⟶ x3) ⟶ (∀ x1 : ο . (wn x1 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ο . x1 ⟶ wn x1 ⟶ x2) ⟶ (∀ x1 x2 . wn (∀ x3 . wceq (cv x3) (cv x1)) ⟶ wceq (cv x1) (cv x2) ⟶ ∀ x3 . wceq (cv x1) (cv x2)) ⟶ (∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3) ⟶ ∀ x2 x3 . x1 x3 x2) ⟶ (∀ x1 : ι → ο . ∀ x2 x3 . wceq (cv x2) (cv x3) ⟶ wcel_wl (λ x4 . x1) ⟶ wcel_wl (λ x4 . x1)) ⟶ (∀ x1 : ι → ι → ο . ∀ x2 . wb (wcel2_wl x1) (∀ x3 . wceq (cv x3) (cv x2) ⟶ wcel_wl (λ x4 . x1 x2))) ⟶ wceq ctotbnd (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wa (wceq (cuni (cv x4)) (cv x1)) (wral (λ x5 . wrex (λ x6 . wceq (cv x5) (co (cv x6) (cv x3) (cfv (cv x2) cbl))) (λ x6 . cv x1)) (λ x5 . cv x4))) (λ x4 . cfn)) (λ x3 . crp)) (λ x2 . cfv (cv x1) cme))) ⟶ wceq cbnd (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wceq (cv x1) (co (cv x3) (cv x4) (cfv (cv x2) cbl))) (λ x4 . crp)) (λ x3 . cv x1)) (λ x2 . cfv (cv x1) cme))) ⟶ wceq cismty (cmpt2 (λ x1 x2 . cuni (crn cxmt)) (λ x1 x2 . cuni (crn cxmt)) (λ x1 x2 . cab (λ x3 . wa (wf1o (cdm (cdm (cv x1))) (cdm (cdm (cv x2))) (cv x3)) (wral (λ x4 . wral (λ x5 . wceq (co (cv x4) (cv x5) (cv x1)) (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) (cv x2))) (λ x5 . cdm (cdm (cv x1)))) (λ x4 . cdm (cdm (cv x1))))))) ⟶ wceq crrn (cmpt (λ x1 . cfn) (λ x1 . cmpt2 (λ x2 x3 . co cr (cv x1) cmap) (λ x2 x3 . co cr (cv x1) cmap) (λ x2 x3 . cfv (csu (cv x1) (λ x4 . co (co (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) cmin) c2 cexp)) csqrt))) ⟶ wceq cass (cab (λ x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wceq (co (co (cv x2) (cv x3) (cv x1)) (cv x4) (cv x1)) (co (cv x2) (co (cv x3) (cv x4) (cv x1)) (cv x1))) (λ x4 . cdm (cdm (cv x1)))) (λ x3 . cdm (cdm (cv x1)))) (λ x2 . cdm (cdm (cv x1))))) ⟶ wceq cexid (cab (λ x1 . wrex (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cv x1)) (cv x3)) (wceq (co (cv x3) (cv x2) (cv x1)) (cv x3))) (λ x3 . cdm (cdm (cv x1)))) (λ x2 . cdm (cdm (cv x1))))) ⟶ wceq cmagm (cab (λ x1 . wex (λ x2 . wf (cxp (cv x2) (cv x2)) (cv x2) (cv x1)))) ⟶ wceq csem (cin cmagm cass) ⟶ x0) ⟶ x0
Theorem df_bj_rrvec : wceq crrvec (crab (λ x0 . wceq (cfv (cv x0) csca) crefld) (λ x0 . clvec)) (proof)
Theorem df_tau : wceq ctau (cinf (cin crp (cima (ccnv ccos) (csn c1))) cr clt) (proof)
Theorem df_finxp : ∀ x0 x1 : ι → ο . wceq (cfinxp x0 x1) (cab (λ x2 . wa (wcel x1 com) (wceq c0 (cfv x1 (crdg (cmpt2 (λ x3 x4 . com) (λ x3 x4 . cvv) (λ x3 x4 . cif (wa (wceq (cv x3) c1o) (wcel (cv x4) x0)) c0 (cif (wcel (cv x4) (cxp cvv x0)) (cop (cuni (cv x3)) (cfv (cv x4) c1st)) (cop (cv x3) (cv x4))))) (cop x1 (cv x2))))))) (proof)
Theorem ax_luk1 : ∀ x0 x1 x2 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x2) ⟶ x0 ⟶ x2 (proof)
Theorem ax_luk2 : ∀ x0 : ο . (wn x0 ⟶ x0) ⟶ x0 (proof)
Theorem ax_luk3 : ∀ x0 x1 : ο . x0 ⟶ wn x0 ⟶ x1 (proof)
Theorem ax_wl_13v : ∀ x0 x1 . wn (∀ x2 . wceq (cv x2) (cv x0)) ⟶ wceq (cv x0) (cv x1) ⟶ ∀ x2 . wceq (cv x0) (cv x1) (proof)
Theorem ax_wl_11v : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2) ⟶ ∀ x1 x2 . x0 x2 x1 (proof)
Theorem ax_wl_8cl : ∀ x0 : ι → ο . ∀ x1 x2 . wceq (cv x1) (cv x2) ⟶ wcel_wl (λ x3 . x0) ⟶ wcel_wl (λ x3 . x0) (proof)
Theorem df_wl_clelv2 : ∀ x0 : ι → ι → ο . ∀ x1 . wb (wcel2_wl x0) (∀ x2 . wceq (cv x2) (cv x1) ⟶ wcel_wl (λ x3 . x0 x1)) (proof)
Theorem df_totbnd : wceq ctotbnd (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wceq (cuni (cv x3)) (cv x0)) (wral (λ x4 . wrex (λ x5 . wceq (cv x4) (co (cv x5) (cv x2) (cfv (cv x1) cbl))) (λ x5 . cv x0)) (λ x4 . cv x3))) (λ x3 . cfn)) (λ x2 . crp)) (λ x1 . cfv (cv x0) cme))) (proof)
Theorem df_bnd : wceq cbnd (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wceq (cv x0) (co (cv x2) (cv x3) (cfv (cv x1) cbl))) (λ x3 . crp)) (λ x2 . cv x0)) (λ x1 . cfv (cv x0) cme))) (proof)
Theorem df_ismty : wceq cismty (cmpt2 (λ x0 x1 . cuni (crn cxmt)) (λ x0 x1 . cuni (crn cxmt)) (λ x0 x1 . cab (λ x2 . wa (wf1o (cdm (cdm (cv x0))) (cdm (cdm (cv x1))) (cv x2)) (wral (λ x3 . wral (λ x4 . wceq (co (cv x3) (cv x4) (cv x0)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cv x1))) (λ x4 . cdm (cdm (cv x0)))) (λ x3 . cdm (cdm (cv x0))))))) (proof)
Theorem df_rrn : wceq crrn (cmpt (λ x0 . cfn) (λ x0 . cmpt2 (λ x1 x2 . co cr (cv x0) cmap) (λ x1 x2 . co cr (cv x0) cmap) (λ x1 x2 . cfv (csu (cv x0) (λ x3 . co (co (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) cmin) c2 cexp)) csqrt))) (proof)
Theorem df_ass : wceq cass (cab (λ x0 . wral (λ x1 . wral (λ x2 . wral (λ x3 . wceq (co (co (cv x1) (cv x2) (cv x0)) (cv x3) (cv x0)) (co (cv x1) (co (cv x2) (cv x3) (cv x0)) (cv x0))) (λ x3 . cdm (cdm (cv x0)))) (λ x2 . cdm (cdm (cv x0)))) (λ x1 . cdm (cdm (cv x0))))) (proof)
Theorem df_exid : wceq cexid (cab (λ x0 . wrex (λ x1 . wral (λ x2 . wa (wceq (co (cv x1) (cv x2) (cv x0)) (cv x2)) (wceq (co (cv x2) (cv x1) (cv x0)) (cv x2))) (λ x2 . cdm (cdm (cv x0)))) (λ x1 . cdm (cdm (cv x0))))) (proof)
Theorem df_mgmOLD : wceq cmagm (cab (λ x0 . wex (λ x1 . wf (cxp (cv x1) (cv x1)) (cv x1) (cv x0)))) (proof)
Theorem df_sgrOLD : wceq csem (cin cmagm cass) (proof)