Proofgold Address

Known df_ssb_b__df_bj_rnf__df_bj_sngl__df_bj_tag__df_bj_proj__df_bj_1upl__df_bj_pr1__df_bj_2upl__df_bj_pr2__df_elwise__df_bj_moore__df_bj_mpt3__df_bj_sethom__df_bj_tophom__df_bj_mgmhom__df_bj_topmgmhom__df_bj_cur__df_bj_unc : ∀ x0 : ο . ((∀ x1 : ι → ο . ∀ x2 . wb (wssb x1 x2) (∀ x3 . wceq (cv x3) (cv x2) ⟶ ∀ x4 . wceq (cv x4) (cv x3) ⟶ x1 x4)) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wb (wrnf x1 x2) (wrex x1 x2 ⟶ wral x1 x2)) ⟶ (∀ x1 : ι → ο . wceq (bj_csngl x1) (cab (λ x2 . wrex (λ x3 . wceq (cv x2) (csn (cv x3))) (λ x3 . x1)))) ⟶ (∀ x1 : ι → ο . wceq (bj_ctag x1) (cun (bj_csngl x1) (csn c0))) ⟶ (∀ x1 x2 : ι → ο . wceq (bj_cproj x1 x2) (cab (λ x3 . wcel (csn (cv x3)) (cima x2 (csn x1))))) ⟶ (∀ x1 : ι → ο . wceq (bj_c1upl x1) (cxp (csn c0) (bj_ctag x1))) ⟶ (∀ x1 : ι → ο . wceq (bj_cpr1 x1) (bj_cproj c0 x1)) ⟶ (∀ x1 x2 : ι → ο . wceq (bj_c2uple x1 x2) (cun (bj_c1upl x1) (cxp (csn c1o) (bj_ctag x2)))) ⟶ (∀ x1 : ι → ο . wceq (bj_cpr2 x1) (bj_cproj c1o x1)) ⟶ wceq celwise (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cvv) (λ x2 x3 . cvv) (λ x2 x3 . cab (λ x4 . wrex (λ x5 . wrex (λ x6 . wceq (cv x4) (co (cv x5) (cv x6) (cv x1))) (λ x6 . cv x3)) (λ x5 . cv x2))))) ⟶ wceq cmoore (cab (λ x1 . wral (λ x2 . wcel (cin (cuni (cv x1)) (cint (cv x2))) (cv x1)) (λ x2 . cpw (cv x1)))) ⟶ (∀ x1 x2 x3 x4 : ι → ι → ι → ι → ο . ∀ x5 x6 . wceq (cmpt3 x1 x2 x3 x4) (copab (λ x7 x8 . wrex (λ x9 . wrex (λ x10 . wrex (λ x11 . wa (wceq (cv x7) (cotp (cv x9) (cv x10) (cv x11))) (wceq (cv x8) (x4 x9 x10 x11))) (x3 x9 x10)) (λ x10 . x2 x9 x10 x6)) (λ x9 . x1 x9 x5 x6)))) ⟶ wceq csethom (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cab (λ x3 . wf (cv x1) (cv x2) (cv x3)))) ⟶ wceq ctophom (cmpt2 (λ x1 x2 . ctps) (λ x1 x2 . ctps) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wcel (cima (ccnv (cv x3)) (cv x4)) (cfv (cv x1) ctopn)) (λ x4 . cfv (cv x2) ctopn)) (λ x3 . co (cfv (cv x1) cbs) (cfv (cv x2) cbs) csethom))) ⟶ wceq cmgmhom (cmpt2 (λ x1 x2 . cmgm) (λ x1 x2 . cmgm) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wceq (cfv (co (cv x4) (cv x5) (cfv (cv x1) cplusg)) (cv x3)) (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) (cfv (cv x2) cplusg))) (λ x5 . cfv (cv x1) cbs)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . co (cfv (cv x1) cbs) (cfv (cv x2) cbs) csethom))) ⟶ wceq ctopmgmhom (cmpt2 (λ x1 x2 . ctmd) (λ x1 x2 . ctmd) (λ x1 x2 . cin (co (cv x1) (cv x2) ctophom) (co (cv x1) (cv x2) cmgmhom))) ⟶ wceq ccur_ (cmpt3 (λ x1 x2 x3 . cvv) (λ x1 x2 x3 . cvv) (λ x1 x2 x3 . cvv) (λ x1 x2 x3 . cmpt (λ x4 . co (cxp (cv x1) (cv x2)) (cv x3) csethom) (λ x4 . cmpt (λ x5 . cv x1) (λ x5 . cmpt (λ x6 . cv x2) (λ x6 . cfv (cop (cv x5) (cv x6)) (cv x4)))))) ⟶ wceq cunc_ (cmpt3 (λ x1 x2 x3 . cvv) (λ x1 x2 x3 . cvv) (λ x1 x2 x3 . cvv) (λ x1 x2 x3 . cmpt (λ x4 . co (cv x1) (co (cv x2) (cv x3) csethom) csethom) (λ x4 . cmpt2 (λ x5 x6 . cv x1) (λ x5 x6 . cv x2) (λ x5 x6 . cfv (cv x6) (cfv (cv x5) (cv x4)))))) ⟶ x0) ⟶ x0
Theorem df_ssb_b : ∀ x0 : ι → ο . ∀ x1 . wb (wssb x0 x1) (∀ x2 . wceq (cv x2) (cv x1) ⟶ ∀ x3 . wceq (cv x3) (cv x2) ⟶ x0 x3) (proof)
Theorem df_bj_rnf : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wb (wrnf x0 x1) (wrex x0 x1 ⟶ wral x0 x1) (proof)
Theorem df_bj_sngl : ∀ x0 : ι → ο . wceq (bj_csngl x0) (cab (λ x1 . wrex (λ x2 . wceq (cv x1) (csn (cv x2))) (λ x2 . x0))) (proof)
Theorem df_bj_tag : ∀ x0 : ι → ο . wceq (bj_ctag x0) (cun (bj_csngl x0) (csn c0)) (proof)
Theorem df_bj_proj : ∀ x0 x1 : ι → ο . wceq (bj_cproj x0 x1) (cab (λ x2 . wcel (csn (cv x2)) (cima x1 (csn x0)))) (proof)
Theorem df_bj_1upl : ∀ x0 : ι → ο . wceq (bj_c1upl x0) (cxp (csn c0) (bj_ctag x0)) (proof)
Theorem df_bj_pr1 : ∀ x0 : ι → ο . wceq (bj_cpr1 x0) (bj_cproj c0 x0) (proof)
Theorem df_bj_2upl : ∀ x0 x1 : ι → ο . wceq (bj_c2uple x0 x1) (cun (bj_c1upl x0) (cxp (csn c1o) (bj_ctag x1))) (proof)
Theorem df_bj_pr2 : ∀ x0 : ι → ο . wceq (bj_cpr2 x0) (bj_cproj c1o x0) (proof)
Theorem df_elwise : wceq celwise (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cab (λ x3 . wrex (λ x4 . wrex (λ x5 . wceq (cv x3) (co (cv x4) (cv x5) (cv x0))) (λ x5 . cv x2)) (λ x4 . cv x1))))) (proof)
Theorem df_bj_moore : wceq cmoore (cab (λ x0 . wral (λ x1 . wcel (cin (cuni (cv x0)) (cint (cv x1))) (cv x0)) (λ x1 . cpw (cv x0)))) (proof)
Theorem df_bj_mpt3 : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ο . ∀ x4 x5 . wceq (cmpt3 x0 x1 x2 x3) (copab (λ x6 x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wa (wceq (cv x6) (cotp (cv x8) (cv x9) (cv x10))) (wceq (cv x7) (x3 x8 x9 x10))) (x2 x8 x9)) (λ x9 . x1 x8 x9 x5)) (λ x8 . x0 x8 x4 x5))) (proof)
Theorem df_bj_sethom : wceq csethom (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cab (λ x2 . wf (cv x0) (cv x1) (cv x2)))) (proof)
Theorem df_bj_tophom : wceq ctophom (cmpt2 (λ x0 x1 . ctps) (λ x0 x1 . ctps) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wcel (cima (ccnv (cv x2)) (cv x3)) (cfv (cv x0) ctopn)) (λ x3 . cfv (cv x1) ctopn)) (λ x2 . co (cfv (cv x0) cbs) (cfv (cv x1) cbs) csethom))) (proof)
Theorem df_bj_mgmhom : wceq cmgmhom (cmpt2 (λ x0 x1 . cmgm) (λ x0 x1 . cmgm) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wceq (cfv (co (cv x3) (cv x4) (cfv (cv x0) cplusg)) (cv x2)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x1) cplusg))) (λ x4 . cfv (cv x0) cbs)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . co (cfv (cv x0) cbs) (cfv (cv x1) cbs) csethom))) (proof)
Theorem df_bj_topmgmhom : wceq ctopmgmhom (cmpt2 (λ x0 x1 . ctmd) (λ x0 x1 . ctmd) (λ x0 x1 . cin (co (cv x0) (cv x1) ctophom) (co (cv x0) (cv x1) cmgmhom))) (proof)
Theorem df_bj_cur : wceq ccur_ (cmpt3 (λ x0 x1 x2 . cvv) (λ x0 x1 x2 . cvv) (λ x0 x1 x2 . cvv) (λ x0 x1 x2 . cmpt (λ x3 . co (cxp (cv x0) (cv x1)) (cv x2) csethom) (λ x3 . cmpt (λ x4 . cv x0) (λ x4 . cmpt (λ x5 . cv x1) (λ x5 . cfv (cop (cv x4) (cv x5)) (cv x3)))))) (proof)
Theorem df_bj_unc : wceq cunc_ (cmpt3 (λ x0 x1 x2 . cvv) (λ x0 x1 x2 . cvv) (λ x0 x1 x2 . cvv) (λ x0 x1 x2 . cmpt (λ x3 . co (cv x0) (co (cv x1) (cv x2) csethom) csethom) (λ x3 . cmpt2 (λ x4 x5 . cv x0) (λ x4 x5 . cv x1) (λ x4 x5 . cfv (cv x5) (cfv (cv x4) (cv x3)))))) (proof)