Proofgold Asset

Known df_cart__df_img__df_domain__df_range__df_cup__df_cap__df_restrict__df_succf__df_apply__df_funpart__df_fullfun__df_ub__df_lb__df_altop__df_altxp__df_ofs__df_transport__df_colinear : ∀ x0 : ο . (wceq ccart (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cpprod cep cep) cvv)))) ⟶ wceq cimg (ccom (cimage (cres (ccom c2nd c1st) (cres c1st (cxp cvv cvv)))) ccart) ⟶ wceq cdomain (cimage (cres c1st (cxp cvv cvv))) ⟶ wceq crange (cimage (cres c2nd (cxp cvv cvv))) ⟶ wceq ccup (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cun (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))) ⟶ wceq ccap (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cin (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))) ⟶ wceq crestrict (ccom ccap (ctxp c1st (ccom ccart (ctxp c2nd (ccom crange c1st))))) ⟶ wceq csuccf (ccom ccup (ctxp cid csingle)) ⟶ wceq capply (ccom (ccom cbigcup cbigcup) (ccom (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cres cep csingles) cvv)))) (ccom (ccom csingle cimg) (cpprod cid csingle)))) ⟶ (∀ x1 : ι → ο . wceq (cfunpart x1) (cres x1 (cdm (cin (ccom (cimage x1) csingle) (cxp cvv csingles))))) ⟶ (∀ x1 : ι → ο . wceq (cfullfn x1) (cun (cfunpart x1) (cxp (cdif cvv (cdm (cfunpart x1))) (csn c0)))) ⟶ (∀ x1 : ι → ο . wceq (cub x1) (cdif (cxp cvv cvv) (ccom (cdif cvv x1) (ccnv cep)))) ⟶ (∀ x1 : ι → ο . wceq (clb x1) (cub (ccnv x1))) ⟶ (∀ x1 x2 : ι → ο . wceq (caltop x1 x2) (cpr (csn x1) (cpr x1 (csn x2)))) ⟶ (∀ x1 x2 : ι → ο . wceq (caltxp x1 x2) (cab (λ x3 . wrex (λ x4 . wrex (λ x5 . wceq (cv x3) (caltop (cv x4) (cv x5))) (λ x5 . x2)) (λ x4 . x1)))) ⟶ wceq cofs (copab (λ x1 x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wrex (λ x11 . w3a (wceq (cv x1) (cop (cop (cv x4) (cv x5)) (cop (cv x6) (cv x7)))) (wceq (cv x2) (cop (cop (cv x8) (cv x9)) (cop (cv x10) (cv x11)))) (w3a (wa (wbr (cv x5) (cop (cv x4) (cv x6)) cbtwn) (wbr (cv x9) (cop (cv x8) (cv x10)) cbtwn)) (wa (wbr (cop (cv x4) (cv x5)) (cop (cv x8) (cv x9)) ccgr) (wbr (cop (cv x5) (cv x6)) (cop (cv x9) (cv x10)) ccgr)) (wa (wbr (cop (cv x4) (cv x7)) (cop (cv x8) (cv x11)) ccgr) (wbr (cop (cv x5) (cv x7)) (cop (cv x9) (cv x11)) ccgr)))) (λ x11 . cfv (cv x3) cee)) (λ x10 . cfv (cv x3) cee)) (λ x9 . cfv (cv x3) cee)) (λ x8 . cfv (cv x3) cee)) (λ x7 . cfv (cv x3) cee)) (λ x6 . cfv (cv x3) cee)) (λ x5 . cfv (cv x3) cee)) (λ x4 . cfv (cv x3) cee)) (λ x3 . cn))) ⟶ wceq ctransport (coprab (λ x1 x2 x3 . wrex (λ x4 . wa (w3a (wcel (cv x1) (cxp (cfv (cv x4) cee) (cfv (cv x4) cee))) (wcel (cv x2) (cxp (cfv (cv x4) cee) (cfv (cv x4) cee))) (wne (cfv (cv x2) c1st) (cfv (cv x2) c2nd))) (wceq (cv x3) (crio (λ x5 . wa (wbr (cfv (cv x2) c2nd) (cop (cfv (cv x2) c1st) (cv x5)) cbtwn) (wbr (cop (cfv (cv x2) c2nd) (cv x5)) (cv x1) ccgr)) (λ x5 . cfv (cv x4) cee)))) (λ x4 . cn))) ⟶ wceq ccolin (ccnv (coprab (λ x1 x2 x3 . wrex (λ x4 . wa (w3a (wcel (cv x3) (cfv (cv x4) cee)) (wcel (cv x1) (cfv (cv x4) cee)) (wcel (cv x2) (cfv (cv x4) cee))) (w3o (wbr (cv x3) (cop (cv x1) (cv x2)) cbtwn) (wbr (cv x1) (cop (cv x2) (cv x3)) cbtwn) (wbr (cv x2) (cop (cv x3) (cv x1)) cbtwn))) (λ x4 . cn)))) ⟶ x0) ⟶ x0
Theorem df_cart : wceq ccart (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cpprod cep cep) cvv)))) (proof)
Theorem df_img : wceq cimg (ccom (cimage (cres (ccom c2nd c1st) (cres c1st (cxp cvv cvv)))) ccart) (proof)
Theorem df_domain : wceq cdomain (cimage (cres c1st (cxp cvv cvv))) (proof)
Theorem df_range : wceq crange (cimage (cres c2nd (cxp cvv cvv))) (proof)
Theorem df_cup : wceq ccup (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cun (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))) (proof)
Theorem df_cap : wceq ccap (cdif (cxp (cxp cvv cvv) cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cin (ccom (ccnv c1st) cep) (ccom (ccnv c2nd) cep)) cvv)))) (proof)
Theorem df_restrict : wceq crestrict (ccom ccap (ctxp c1st (ccom ccart (ctxp c2nd (ccom crange c1st))))) (proof)
Theorem df_succf : wceq csuccf (ccom ccup (ctxp cid csingle)) (proof)
Theorem df_apply : wceq capply (ccom (ccom cbigcup cbigcup) (ccom (cdif (cxp cvv cvv) (crn (csymdif (ctxp cvv cep) (ctxp (cres cep csingles) cvv)))) (ccom (ccom csingle cimg) (cpprod cid csingle)))) (proof)
Theorem df_funpart : ∀ x0 : ι → ο . wceq (cfunpart x0) (cres x0 (cdm (cin (ccom (cimage x0) csingle) (cxp cvv csingles)))) (proof)
Theorem df_fullfun : ∀ x0 : ι → ο . wceq (cfullfn x0) (cun (cfunpart x0) (cxp (cdif cvv (cdm (cfunpart x0))) (csn c0))) (proof)
Theorem df_ub : ∀ x0 : ι → ο . wceq (cub x0) (cdif (cxp cvv cvv) (ccom (cdif cvv x0) (ccnv cep))) (proof)
Theorem df_lb : ∀ x0 : ι → ο . wceq (clb x0) (cub (ccnv x0)) (proof)
Theorem df_altop : ∀ x0 x1 : ι → ο . wceq (caltop x0 x1) (cpr (csn x0) (cpr x0 (csn x1))) (proof)
Theorem df_altxp : ∀ x0 x1 : ι → ο . wceq (caltxp x0 x1) (cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (caltop (cv x3) (cv x4))) (λ x4 . x1)) (λ x3 . x0))) (proof)
Theorem df_ofs : wceq cofs (copab (λ x0 x1 . wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wrex (λ x5 . wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . w3a (wceq (cv x0) (cop (cop (cv x3) (cv x4)) (cop (cv x5) (cv x6)))) (wceq (cv x1) (cop (cop (cv x7) (cv x8)) (cop (cv x9) (cv x10)))) (w3a (wa (wbr (cv x4) (cop (cv x3) (cv x5)) cbtwn) (wbr (cv x8) (cop (cv x7) (cv x9)) cbtwn)) (wa (wbr (cop (cv x3) (cv x4)) (cop (cv x7) (cv x8)) ccgr) (wbr (cop (cv x4) (cv x5)) (cop (cv x8) (cv x9)) ccgr)) (wa (wbr (cop (cv x3) (cv x6)) (cop (cv x7) (cv x10)) ccgr) (wbr (cop (cv x4) (cv x6)) (cop (cv x8) (cv x10)) ccgr)))) (λ x10 . cfv (cv x2) cee)) (λ x9 . cfv (cv x2) cee)) (λ x8 . cfv (cv x2) cee)) (λ x7 . cfv (cv x2) cee)) (λ x6 . cfv (cv x2) cee)) (λ x5 . cfv (cv x2) cee)) (λ x4 . cfv (cv x2) cee)) (λ x3 . cfv (cv x2) cee)) (λ x2 . cn))) (proof)
Theorem df_transport : wceq ctransport (coprab (λ x0 x1 x2 . wrex (λ x3 . wa (w3a (wcel (cv x0) (cxp (cfv (cv x3) cee) (cfv (cv x3) cee))) (wcel (cv x1) (cxp (cfv (cv x3) cee) (cfv (cv x3) cee))) (wne (cfv (cv x1) c1st) (cfv (cv x1) c2nd))) (wceq (cv x2) (crio (λ x4 . wa (wbr (cfv (cv x1) c2nd) (cop (cfv (cv x1) c1st) (cv x4)) cbtwn) (wbr (cop (cfv (cv x1) c2nd) (cv x4)) (cv x0) ccgr)) (λ x4 . cfv (cv x3) cee)))) (λ x3 . cn))) (proof)
Theorem df_colinear : wceq ccolin (ccnv (coprab (λ x0 x1 x2 . wrex (λ x3 . wa (w3a (wcel (cv x2) (cfv (cv x3) cee)) (wcel (cv x0) (cfv (cv x3) cee)) (wcel (cv x1) (cfv (cv x3) cee))) (w3o (wbr (cv x2) (cop (cv x0) (cv x1)) cbtwn) (wbr (cv x0) (cop (cv x1) (cv x2)) cbtwn) (wbr (cv x1) (cop (cv x2) (cv x0)) cbtwn))) (λ x3 . cn)))) (proof)