Proofgold Asset

Known df_fn__df_f__df_f1__df_fo__df_f1o__df_fv__df_isom__df_riota__df_ov__df_oprab__df_mpt2__df_of__df_ofr__df_rpss__ax_un__df_om__df_1st__df_2nd : ∀ x0 : ο . ((∀ x1 x2 : ι → ο . wb (wfn x1 x2) (wa (wfun x1) (wceq (cdm x1) x2))) ⟶ (∀ x1 x2 x3 : ι → ο . wb (wf x1 x2 x3) (wa (wfn x3 x1) (wss (crn x3) x2))) ⟶ (∀ x1 x2 x3 : ι → ο . wb (wf1 x1 x2 x3) (wa (wf x1 x2 x3) (wfun (ccnv x3)))) ⟶ (∀ x1 x2 x3 : ι → ο . wb (wfo x1 x2 x3) (wa (wfn x3 x1) (wceq (crn x3) x2))) ⟶ (∀ x1 x2 x3 : ι → ο . wb (wf1o x1 x2 x3) (wa (wf1 x1 x2 x3) (wfo x1 x2 x3))) ⟶ (∀ x1 x2 : ι → ο . wceq (cfv x1 x2) (cio (λ x3 . wbr x1 (cv x3) x2))) ⟶ (∀ x1 x2 x3 x4 x5 : ι → ο . wb (wiso x1 x2 x3 x4 x5) (wa (wf1o x1 x2 x5) (wral (λ x6 . wral (λ x7 . wb (wbr (cv x6) (cv x7) x3) (wbr (cfv (cv x6) x5) (cfv (cv x7) x5) x4)) (λ x7 . x1)) (λ x6 . x1)))) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wceq (crio x1 x2) (cio (λ x3 . wa (wcel (cv x3) (x2 x3)) (x1 x3)))) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (co x1 x2 x3) (cfv (cop x1 x2) x3)) ⟶ (∀ x1 : ι → ι → ι → ο . wceq (coprab x1) (cab (λ x2 . wex (λ x3 . wex (λ x4 . wex (λ x5 . wa (wceq (cv x2) (cop (cop (cv x3) (cv x4)) (cv x5))) (x1 x3 x4 x5))))))) ⟶ (∀ x1 x2 x3 : ι → ι → ι → ο . wceq (cmpt2 x1 x2 x3) (coprab (λ x4 x5 x6 . wa (wa (wcel (cv x4) (x1 x4 x5)) (wcel (cv x5) (x2 x4 x5))) (wceq (cv x6) (x3 x4 x5))))) ⟶ (∀ x1 : ι → ο . wceq (cof x1) (cmpt2 (λ x2 x3 . cvv) (λ x2 x3 . cvv) (λ x2 x3 . cmpt (λ x4 . cin (cdm (cv x2)) (cdm (cv x3))) (λ x4 . co (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) x1)))) ⟶ (∀ x1 : ι → ο . wceq (cofr x1) (copab (λ x2 x3 . wral (λ x4 . wbr (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) x1) (λ x4 . cin (cdm (cv x2)) (cdm (cv x3)))))) ⟶ wceq crpss (copab (λ x1 x2 . wpss (cv x1) (cv x2))) ⟶ (∀ x1 . wex (λ x2 . ∀ x3 . wex (λ x4 . wa (wcel (cv x3) (cv x4)) (wcel (cv x4) (cv x1))) ⟶ wcel (cv x3) (cv x2))) ⟶ wceq com (crab (λ x1 . ∀ x2 . wlim (cv x2) ⟶ wcel (cv x1) (cv x2)) (λ x1 . con0)) ⟶ wceq c1st (cmpt (λ x1 . cvv) (λ x1 . cuni (cdm (csn (cv x1))))) ⟶ wceq c2nd (cmpt (λ x1 . cvv) (λ x1 . cuni (crn (csn (cv x1))))) ⟶ x0) ⟶ x0
Theorem df_fn : ∀ x0 x1 : ι → ο . wb (wfn x0 x1) (wa (wfun x0) (wceq (cdm x0) x1)) (proof)
Theorem df_f : ∀ x0 x1 x2 : ι → ο . wb (wf x0 x1 x2) (wa (wfn x2 x0) (wss (crn x2) x1)) (proof)
Theorem df_f1 : ∀ x0 x1 x2 : ι → ο . wb (wf1 x0 x1 x2) (wa (wf x0 x1 x2) (wfun (ccnv x2))) (proof)
Theorem df_fo : ∀ x0 x1 x2 : ι → ο . wb (wfo x0 x1 x2) (wa (wfn x2 x0) (wceq (crn x2) x1)) (proof)
Theorem df_f1o : ∀ x0 x1 x2 : ι → ο . wb (wf1o x0 x1 x2) (wa (wf1 x0 x1 x2) (wfo x0 x1 x2)) (proof)
Theorem df_fv : ∀ x0 x1 : ι → ο . wceq (cfv x0 x1) (cio (λ x2 . wbr x0 (cv x2) x1)) (proof)
Theorem df_isom : ∀ x0 x1 x2 x3 x4 : ι → ο . wb (wiso x0 x1 x2 x3 x4) (wa (wf1o x0 x1 x4) (wral (λ x5 . wral (λ x6 . wb (wbr (cv x5) (cv x6) x2) (wbr (cfv (cv x5) x4) (cfv (cv x6) x4) x3)) (λ x6 . x0)) (λ x5 . x0))) (proof)
Theorem df_riota : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wceq (crio x0 x1) (cio (λ x2 . wa (wcel (cv x2) (x1 x2)) (x0 x2))) (proof)
Theorem df_ov : ∀ x0 x1 x2 : ι → ο . wceq (co x0 x1 x2) (cfv (cop x0 x1) x2) (proof)
Theorem df_oprab : ∀ x0 : ι → ι → ι → ο . wceq (coprab x0) (cab (λ x1 . wex (λ x2 . wex (λ x3 . wex (λ x4 . wa (wceq (cv x1) (cop (cop (cv x2) (cv x3)) (cv x4))) (x0 x2 x3 x4)))))) (proof)
Theorem df_mpt2 : ∀ x0 x1 x2 : ι → ι → ι → ο . wceq (cmpt2 x0 x1 x2) (coprab (λ x3 x4 x5 . wa (wa (wcel (cv x3) (x0 x3 x4)) (wcel (cv x4) (x1 x3 x4))) (wceq (cv x5) (x2 x3 x4)))) (proof)
Theorem df_of : ∀ x0 : ι → ο . wceq (cof x0) (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cin (cdm (cv x1)) (cdm (cv x2))) (λ x3 . co (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) x0))) (proof)
Theorem df_ofr : ∀ x0 : ι → ο . wceq (cofr x0) (copab (λ x1 x2 . wral (λ x3 . wbr (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) x0) (λ x3 . cin (cdm (cv x1)) (cdm (cv x2))))) (proof)
Theorem df_rpss : wceq crpss (copab (λ x0 x1 . wpss (cv x0) (cv x1))) (proof)
Theorem ax_un : ∀ x0 . wex (λ x1 . ∀ x2 . wex (λ x3 . wa (wcel (cv x2) (cv x3)) (wcel (cv x3) (cv x0))) ⟶ wcel (cv x2) (cv x1)) (proof)
Theorem df_om : wceq com (crab (λ x0 . ∀ x1 . wlim (cv x1) ⟶ wcel (cv x0) (cv x1)) (λ x0 . con0)) (proof)
Theorem df_1st : wceq c1st (cmpt (λ x0 . cvv) (λ x0 . cuni (cdm (csn (cv x0))))) (proof)
Theorem df_2nd : wceq c2nd (cmpt (λ x0 . cvv) (λ x0 . cuni (crn (csn (cv x0))))) (proof)