Proofgold Asset

Known df_inv__df_iso__df_cic__df_ssc__df_resc__df_subc__df_func__df_idfu__df_cofu__df_resf__df_full__df_fth__df_nat__df_fuc__df_inito__df_termo__df_zeroo__df_doma : ∀ x0 : ο . (wceq cinv (cmpt (λ x1 . ccat) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cin (co (cv x2) (cv x3) (cfv (cv x1) csect)) (ccnv (co (cv x3) (cv x2) (cfv (cv x1) csect)))))) ⟶ wceq ciso (cmpt (λ x1 . ccat) (λ x1 . ccom (cmpt (λ x2 . cvv) (λ x2 . cdm (cv x2))) (cfv (cv x1) cinv))) ⟶ wceq ccic (cmpt (λ x1 . ccat) (λ x1 . co (cfv (cv x1) ciso) c0 csupp)) ⟶ wceq cssc (copab (λ x1 x2 . wex (λ x3 . wa (wfn (cv x2) (cxp (cv x3) (cv x3))) (wrex (λ x4 . wcel (cv x1) (cixp (λ x5 . cxp (cv x4) (cv x4)) (λ x5 . cpw (cfv (cv x5) (cv x2))))) (λ x4 . cpw (cv x3)))))) ⟶ wceq cresc (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (co (cv x1) (cdm (cdm (cv x2))) cress) (cop (cfv cnx chom) (cv x2)) csts)) ⟶ wceq csubc (cmpt (λ x1 . ccat) (λ x1 . cab (λ x2 . wa (wbr (cv x2) (cfv (cv x1) chomf) cssc) (wsbc (λ x3 . wral (λ x4 . wa (wcel (cfv (cv x4) (cfv (cv x1) ccid)) (co (cv x4) (cv x4) (cv x2))) (wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wcel (co (cv x8) (cv x7) (co (cop (cv x4) (cv x5)) (cv x6) (cfv (cv x1) cco))) (co (cv x4) (cv x6) (cv x2))) (λ x8 . co (cv x5) (cv x6) (cv x2))) (λ x7 . co (cv x4) (cv x5) (cv x2))) (λ x6 . cv x3)) (λ x5 . cv x3))) (λ x4 . cv x3)) (cdm (cdm (cv x2))))))) ⟶ wceq cfunc (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . copab (λ x3 x4 . wsbc (λ x5 . w3a (wf (cv x5) (cfv (cv x2) cbs) (cv x3)) (wcel (cv x4) (cixp (λ x6 . cxp (cv x5) (cv x5)) (λ x6 . co (co (cfv (cfv (cv x6) c1st) (cv x3)) (cfv (cfv (cv x6) c2nd) (cv x3)) (cfv (cv x2) chom)) (cfv (cv x6) (cfv (cv x1) chom)) cmap))) (wral (λ x6 . wa (wceq (cfv (cfv (cv x6) (cfv (cv x1) ccid)) (co (cv x6) (cv x6) (cv x4))) (cfv (cfv (cv x6) (cv x3)) (cfv (cv x2) ccid))) (wral (λ x7 . wral (λ x8 . wral (λ x9 . wral (λ x10 . wceq (cfv (co (cv x10) (cv x9) (co (cop (cv x6) (cv x7)) (cv x8) (cfv (cv x1) cco))) (co (cv x6) (cv x8) (cv x4))) (co (cfv (cv x10) (co (cv x7) (cv x8) (cv x4))) (cfv (cv x9) (co (cv x6) (cv x7) (cv x4))) (co (cop (cfv (cv x6) (cv x3)) (cfv (cv x7) (cv x3))) (cfv (cv x8) (cv x3)) (cfv (cv x2) cco)))) (λ x10 . co (cv x7) (cv x8) (cfv (cv x1) chom))) (λ x9 . co (cv x6) (cv x7) (cfv (cv x1) chom))) (λ x8 . cv x5)) (λ x7 . cv x5))) (λ x6 . cv x5))) (cfv (cv x1) cbs)))) ⟶ wceq cidfu (cmpt (λ x1 . ccat) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . cop (cres cid (cv x2)) (cmpt (λ x3 . cxp (cv x2) (cv x2)) (λ x3 . cres cid (cfv (cv x3) (cfv (cv x1) chom))))))) ⟶ wceq ccofu (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cop (ccom (cfv (cv x1) c1st) (cfv (cv x2) c1st)) (cmpt2 (λ x3 x4 . cdm (cdm (cfv (cv x2) c2nd))) (λ x3 x4 . cdm (cdm (cfv (cv x2) c2nd))) (λ x3 x4 . ccom (co (cfv (cv x3) (cfv (cv x2) c1st)) (cfv (cv x4) (cfv (cv x2) c1st)) (cfv (cv x1) c2nd)) (co (cv x3) (cv x4) (cfv (cv x2) c2nd)))))) ⟶ wceq cresf (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cop (cres (cfv (cv x1) c1st) (cdm (cdm (cv x2)))) (cmpt (λ x3 . cdm (cv x2)) (λ x3 . cres (cfv (cv x3) (cfv (cv x1) c2nd)) (cfv (cv x3) (cv x2)))))) ⟶ wceq cful (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . copab (λ x3 x4 . wa (wbr (cv x3) (cv x4) (co (cv x1) (cv x2) cfunc)) (wral (λ x5 . wral (λ x6 . wceq (crn (co (cv x5) (cv x6) (cv x4))) (co (cfv (cv x5) (cv x3)) (cfv (cv x6) (cv x3)) (cfv (cv x2) chom))) (λ x6 . cfv (cv x1) cbs)) (λ x5 . cfv (cv x1) cbs))))) ⟶ wceq cfth (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . copab (λ x3 x4 . wa (wbr (cv x3) (cv x4) (co (cv x1) (cv x2) cfunc)) (wral (λ x5 . wral (λ x6 . wfun (ccnv (co (cv x5) (cv x6) (cv x4)))) (λ x6 . cfv (cv x1) cbs)) (λ x5 . cfv (cv x1) cbs))))) ⟶ wceq cnat (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . cmpt2 (λ x3 x4 . co (cv x1) (cv x2) cfunc) (λ x3 x4 . co (cv x1) (cv x2) cfunc) (λ x3 x4 . csb (cfv (cv x3) c1st) (λ x5 . csb (cfv (cv x4) c1st) (λ x6 . crab (λ x7 . wral (λ x8 . wral (λ x9 . wral (λ x10 . wceq (co (cfv (cv x9) (cv x7)) (cfv (cv x10) (co (cv x8) (cv x9) (cfv (cv x3) c2nd))) (co (cop (cfv (cv x8) (cv x5)) (cfv (cv x9) (cv x5))) (cfv (cv x9) (cv x6)) (cfv (cv x2) cco))) (co (cfv (cv x10) (co (cv x8) (cv x9) (cfv (cv x4) c2nd))) (cfv (cv x8) (cv x7)) (co (cop (cfv (cv x8) (cv x5)) (cfv (cv x8) (cv x6))) (cfv (cv x9) (cv x6)) (cfv (cv x2) cco)))) (λ x10 . co (cv x8) (cv x9) (cfv (cv x1) chom))) (λ x9 . cfv (cv x1) cbs)) (λ x8 . cfv (cv x1) cbs)) (λ x7 . cixp (λ x8 . cfv (cv x1) cbs) (λ x8 . co (cfv (cv x8) (cv x5)) (cfv (cv x8) (cv x6)) (cfv (cv x2) chom)))))))) ⟶ wceq cfuc (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . ctp (cop (cfv cnx cbs) (co (cv x1) (cv x2) cfunc)) (cop (cfv cnx chom) (co (cv x1) (cv x2) cnat)) (cop (cfv cnx cco) (cmpt2 (λ x3 x4 . cxp (co (cv x1) (cv x2) cfunc) (co (cv x1) (cv x2) cfunc)) (λ x3 x4 . co (cv x1) (cv x2) cfunc) (λ x3 x4 . csb (cfv (cv x3) c1st) (λ x5 . csb (cfv (cv x3) c2nd) (λ x6 . cmpt2 (λ x7 x8 . co (cv x6) (cv x4) (co (cv x1) (cv x2) cnat)) (λ x7 x8 . co (cv x5) (cv x6) (co (cv x1) (cv x2) cnat)) (λ x7 x8 . cmpt (λ x9 . cfv (cv x1) cbs) (λ x9 . co (cfv (cv x9) (cv x7)) (cfv (cv x9) (cv x8)) (co (cop (cfv (cv x9) (cfv (cv x5) c1st)) (cfv (cv x9) (cfv (cv x6) c1st))) (cfv (cv x9) (cfv (cv x4) c1st)) (cfv (cv x2) cco))))))))))) ⟶ wceq cinito (cmpt (λ x1 . ccat) (λ x1 . crab (λ x2 . wral (λ x3 . weu (λ x4 . wcel (cv x4) (co (cv x2) (cv x3) (cfv (cv x1) chom)))) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs))) ⟶ wceq ctermo (cmpt (λ x1 . ccat) (λ x1 . crab (λ x2 . wral (λ x3 . weu (λ x4 . wcel (cv x4) (co (cv x3) (cv x2) (cfv (cv x1) chom)))) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs))) ⟶ wceq czeroo (cmpt (λ x1 . ccat) (λ x1 . cin (cfv (cv x1) cinito) (cfv (cv x1) ctermo))) ⟶ wceq cdoma (ccom c1st c1st) ⟶ x0) ⟶ x0
Theorem df_inv : wceq cinv (cmpt (λ x0 . ccat) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cin (co (cv x1) (cv x2) (cfv (cv x0) csect)) (ccnv (co (cv x2) (cv x1) (cfv (cv x0) csect)))))) (proof)
Theorem df_iso : wceq ciso (cmpt (λ x0 . ccat) (λ x0 . ccom (cmpt (λ x1 . cvv) (λ x1 . cdm (cv x1))) (cfv (cv x0) cinv))) (proof)
Theorem df_cic : wceq ccic (cmpt (λ x0 . ccat) (λ x0 . co (cfv (cv x0) ciso) c0 csupp)) (proof)
Theorem df_ssc : wceq cssc (copab (λ x0 x1 . wex (λ x2 . wa (wfn (cv x1) (cxp (cv x2) (cv x2))) (wrex (λ x3 . wcel (cv x0) (cixp (λ x4 . cxp (cv x3) (cv x3)) (λ x4 . cpw (cfv (cv x4) (cv x1))))) (λ x3 . cpw (cv x2)))))) (proof)
Theorem df_resc : wceq cresc (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cv x0) (cdm (cdm (cv x1))) cress) (cop (cfv cnx chom) (cv x1)) csts)) (proof)
Theorem df_subc : wceq csubc (cmpt (λ x0 . ccat) (λ x0 . cab (λ x1 . wa (wbr (cv x1) (cfv (cv x0) chomf) cssc) (wsbc (λ x2 . wral (λ x3 . wa (wcel (cfv (cv x3) (cfv (cv x0) ccid)) (co (cv x3) (cv x3) (cv x1))) (wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wcel (co (cv x7) (cv x6) (co (cop (cv x3) (cv x4)) (cv x5) (cfv (cv x0) cco))) (co (cv x3) (cv x5) (cv x1))) (λ x7 . co (cv x4) (cv x5) (cv x1))) (λ x6 . co (cv x3) (cv x4) (cv x1))) (λ x5 . cv x2)) (λ x4 . cv x2))) (λ x3 . cv x2)) (cdm (cdm (cv x1))))))) (proof)
Theorem df_func : wceq cfunc (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . copab (λ x2 x3 . wsbc (λ x4 . w3a (wf (cv x4) (cfv (cv x1) cbs) (cv x2)) (wcel (cv x3) (cixp (λ x5 . cxp (cv x4) (cv x4)) (λ x5 . co (co (cfv (cfv (cv x5) c1st) (cv x2)) (cfv (cfv (cv x5) c2nd) (cv x2)) (cfv (cv x1) chom)) (cfv (cv x5) (cfv (cv x0) chom)) cmap))) (wral (λ x5 . wa (wceq (cfv (cfv (cv x5) (cfv (cv x0) ccid)) (co (cv x5) (cv x5) (cv x3))) (cfv (cfv (cv x5) (cv x2)) (cfv (cv x1) ccid))) (wral (λ x6 . wral (λ x7 . wral (λ x8 . wral (λ x9 . wceq (cfv (co (cv x9) (cv x8) (co (cop (cv x5) (cv x6)) (cv x7) (cfv (cv x0) cco))) (co (cv x5) (cv x7) (cv x3))) (co (cfv (cv x9) (co (cv x6) (cv x7) (cv x3))) (cfv (cv x8) (co (cv x5) (cv x6) (cv x3))) (co (cop (cfv (cv x5) (cv x2)) (cfv (cv x6) (cv x2))) (cfv (cv x7) (cv x2)) (cfv (cv x1) cco)))) (λ x9 . co (cv x6) (cv x7) (cfv (cv x0) chom))) (λ x8 . co (cv x5) (cv x6) (cfv (cv x0) chom))) (λ x7 . cv x4)) (λ x6 . cv x4))) (λ x5 . cv x4))) (cfv (cv x0) cbs)))) (proof)
Theorem df_idfu : wceq cidfu (cmpt (λ x0 . ccat) (λ x0 . csb (cfv (cv x0) cbs) (λ x1 . cop (cres cid (cv x1)) (cmpt (λ x2 . cxp (cv x1) (cv x1)) (λ x2 . cres cid (cfv (cv x2) (cfv (cv x0) chom))))))) (proof)
Theorem df_cofu : wceq ccofu (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cop (ccom (cfv (cv x0) c1st) (cfv (cv x1) c1st)) (cmpt2 (λ x2 x3 . cdm (cdm (cfv (cv x1) c2nd))) (λ x2 x3 . cdm (cdm (cfv (cv x1) c2nd))) (λ x2 x3 . ccom (co (cfv (cv x2) (cfv (cv x1) c1st)) (cfv (cv x3) (cfv (cv x1) c1st)) (cfv (cv x0) c2nd)) (co (cv x2) (cv x3) (cfv (cv x1) c2nd)))))) (proof)
Theorem df_resf : wceq cresf (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cop (cres (cfv (cv x0) c1st) (cdm (cdm (cv x1)))) (cmpt (λ x2 . cdm (cv x1)) (λ x2 . cres (cfv (cv x2) (cfv (cv x0) c2nd)) (cfv (cv x2) (cv x1)))))) (proof)
Theorem df_full : wceq cful (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . copab (λ x2 x3 . wa (wbr (cv x2) (cv x3) (co (cv x0) (cv x1) cfunc)) (wral (λ x4 . wral (λ x5 . wceq (crn (co (cv x4) (cv x5) (cv x3))) (co (cfv (cv x4) (cv x2)) (cfv (cv x5) (cv x2)) (cfv (cv x1) chom))) (λ x5 . cfv (cv x0) cbs)) (λ x4 . cfv (cv x0) cbs))))) (proof)
Theorem df_fth : wceq cfth (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . copab (λ x2 x3 . wa (wbr (cv x2) (cv x3) (co (cv x0) (cv x1) cfunc)) (wral (λ x4 . wral (λ x5 . wfun (ccnv (co (cv x4) (cv x5) (cv x3)))) (λ x5 . cfv (cv x0) cbs)) (λ x4 . cfv (cv x0) cbs))))) (proof)
Theorem df_nat : wceq cnat (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . cmpt2 (λ x2 x3 . co (cv x0) (cv x1) cfunc) (λ x2 x3 . co (cv x0) (cv x1) cfunc) (λ x2 x3 . csb (cfv (cv x2) c1st) (λ x4 . csb (cfv (cv x3) c1st) (λ x5 . crab (λ x6 . wral (λ x7 . wral (λ x8 . wral (λ x9 . wceq (co (cfv (cv x8) (cv x6)) (cfv (cv x9) (co (cv x7) (cv x8) (cfv (cv x2) c2nd))) (co (cop (cfv (cv x7) (cv x4)) (cfv (cv x8) (cv x4))) (cfv (cv x8) (cv x5)) (cfv (cv x1) cco))) (co (cfv (cv x9) (co (cv x7) (cv x8) (cfv (cv x3) c2nd))) (cfv (cv x7) (cv x6)) (co (cop (cfv (cv x7) (cv x4)) (cfv (cv x7) (cv x5))) (cfv (cv x8) (cv x5)) (cfv (cv x1) cco)))) (λ x9 . co (cv x7) (cv x8) (cfv (cv x0) chom))) (λ x8 . cfv (cv x0) cbs)) (λ x7 . cfv (cv x0) cbs)) (λ x6 . cixp (λ x7 . cfv (cv x0) cbs) (λ x7 . co (cfv (cv x7) (cv x4)) (cfv (cv x7) (cv x5)) (cfv (cv x1) chom)))))))) (proof)
Theorem df_fuc : wceq cfuc (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . ctp (cop (cfv cnx cbs) (co (cv x0) (cv x1) cfunc)) (cop (cfv cnx chom) (co (cv x0) (cv x1) cnat)) (cop (cfv cnx cco) (cmpt2 (λ x2 x3 . cxp (co (cv x0) (cv x1) cfunc) (co (cv x0) (cv x1) cfunc)) (λ x2 x3 . co (cv x0) (cv x1) cfunc) (λ x2 x3 . csb (cfv (cv x2) c1st) (λ x4 . csb (cfv (cv x2) c2nd) (λ x5 . cmpt2 (λ x6 x7 . co (cv x5) (cv x3) (co (cv x0) (cv x1) cnat)) (λ x6 x7 . co (cv x4) (cv x5) (co (cv x0) (cv x1) cnat)) (λ x6 x7 . cmpt (λ x8 . cfv (cv x0) cbs) (λ x8 . co (cfv (cv x8) (cv x6)) (cfv (cv x8) (cv x7)) (co (cop (cfv (cv x8) (cfv (cv x4) c1st)) (cfv (cv x8) (cfv (cv x5) c1st))) (cfv (cv x8) (cfv (cv x3) c1st)) (cfv (cv x1) cco))))))))))) (proof)
Theorem df_inito : wceq cinito (cmpt (λ x0 . ccat) (λ x0 . crab (λ x1 . wral (λ x2 . weu (λ x3 . wcel (cv x3) (co (cv x1) (cv x2) (cfv (cv x0) chom)))) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs))) (proof)
Theorem df_termo : wceq ctermo (cmpt (λ x0 . ccat) (λ x0 . crab (λ x1 . wral (λ x2 . weu (λ x3 . wcel (cv x3) (co (cv x2) (cv x1) (cfv (cv x0) chom)))) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs))) (proof)
Theorem df_zeroo : wceq czeroo (cmpt (λ x0 . ccat) (λ x0 . cin (cfv (cv x0) cinito) (cfv (cv x0) ctermo))) (proof)
Theorem df_doma : wceq cdoma (ccom c1st c1st) (proof)