Proofgold Address

Known ax_inf2__df_cnf__df_tc__df_r1__df_rank__df_card__df_aleph__df_cf__df_acn__df_ac__df_cda__df_fin1a__df_fin2__df_fin4__df_fin3__df_fin5__df_fin6__df_fin7 : ∀ x0 : ο . (wex (λ x1 . wa (wex (λ x2 . wa (wcel (cv x2) (cv x1)) (∀ x3 . wn (wcel (cv x3) (cv x2))))) (∀ x2 . wcel (cv x2) (cv x1) ⟶ wex (λ x3 . wa (wcel (cv x3) (cv x1)) (∀ x4 . wb (wcel (cv x4) (cv x3)) (wo (wcel (cv x4) (cv x2)) (wceq (cv x4) (cv x2))))))) ⟶ wceq ccnf (cmpt2 (λ x1 x2 . con0) (λ x1 x2 . con0) (λ x1 x2 . cmpt (λ x3 . crab (λ x4 . wbr (cv x4) c0 cfsupp) (λ x4 . co (cv x1) (cv x2) cmap)) (λ x3 . csb (coi (co (cv x3) c0 csupp) cep) (λ x4 . cfv (cdm (cv x4)) (cseqom (cmpt2 (λ x5 x6 . cvv) (λ x5 x6 . cvv) (λ x5 x6 . co (co (co (cv x1) (cfv (cv x5) (cv x4)) coe) (cfv (cfv (cv x5) (cv x4)) (cv x3)) comu) (cv x6) coa)) c0))))) ⟶ wceq ctc (cmpt (λ x1 . cvv) (λ x1 . cint (cab (λ x2 . wa (wss (cv x1) (cv x2)) (wtr (cv x2)))))) ⟶ wceq cr1 (crdg (cmpt (λ x1 . cvv) (λ x1 . cpw (cv x1))) c0) ⟶ wceq crnk (cmpt (λ x1 . cvv) (λ x1 . cint (crab (λ x2 . wcel (cv x1) (cfv (csuc (cv x2)) cr1)) (λ x2 . con0)))) ⟶ wceq ccrd (cmpt (λ x1 . cvv) (λ x1 . cint (crab (λ x2 . wbr (cv x2) (cv x1) cen) (λ x2 . con0)))) ⟶ wceq cale (crdg char com) ⟶ wceq ccf (cmpt (λ x1 . con0) (λ x1 . cint (cab (λ x2 . wex (λ x3 . wa (wceq (cv x2) (cfv (cv x3) ccrd)) (wa (wss (cv x3) (cv x1)) (wral (λ x4 . wrex (λ x5 . wss (cv x4) (cv x5)) (λ x5 . cv x3)) (λ x4 . cv x1)))))))) ⟶ (∀ x1 : ι → ο . wceq (wacn x1) (cab (λ x2 . wa (wcel x1 cvv) (wral (λ x3 . wex (λ x4 . wral (λ x5 . wcel (cfv (cv x5) (cv x4)) (cfv (cv x5) (cv x3))) (λ x5 . x1))) (λ x3 . co (cdif (cpw (cv x2)) (csn c0)) x1 cmap))))) ⟶ wb wac (∀ x1 . wex (λ x2 . wa (wss (cv x2) (cv x1)) (wfn (cv x2) (cdm (cv x1))))) ⟶ wceq ccda (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cun (cxp (cv x1) (csn c0)) (cxp (cv x2) (csn c1o)))) ⟶ wceq cfin1a (cab (λ x1 . wral (λ x2 . wo (wcel (cv x2) cfn) (wcel (cdif (cv x1) (cv x2)) cfn)) (λ x2 . cpw (cv x1)))) ⟶ wceq cfin2 (cab (λ x1 . wral (λ x2 . wa (wne (cv x2) c0) (wor (cv x2) crpss) ⟶ wcel (cuni (cv x2)) (cv x2)) (λ x2 . cpw (cpw (cv x1))))) ⟶ wceq cfin4 (cab (λ x1 . wn (wex (λ x2 . wa (wpss (cv x2) (cv x1)) (wbr (cv x2) (cv x1) cen))))) ⟶ wceq cfin3 (cab (λ x1 . wcel (cpw (cv x1)) cfin4)) ⟶ wceq cfin5 (cab (λ x1 . wo (wceq (cv x1) c0) (wbr (cv x1) (co (cv x1) (cv x1) ccda) csdm))) ⟶ wceq cfin6 (cab (λ x1 . wo (wbr (cv x1) c2o csdm) (wbr (cv x1) (cxp (cv x1) (cv x1)) csdm))) ⟶ wceq cfin7 (cab (λ x1 . wn (wrex (λ x2 . wbr (cv x1) (cv x2) cen) (λ x2 . cdif con0 com)))) ⟶ x0) ⟶ x0
Theorem ax_inf2 : wex (λ x0 . wa (wex (λ x1 . wa (wcel (cv x1) (cv x0)) (∀ x2 . wn (wcel (cv x2) (cv x1))))) (∀ x1 . wcel (cv x1) (cv x0) ⟶ wex (λ x2 . wa (wcel (cv x2) (cv x0)) (∀ x3 . wb (wcel (cv x3) (cv x2)) (wo (wcel (cv x3) (cv x1)) (wceq (cv x3) (cv x1))))))) (proof)
Theorem df_cnf : wceq ccnf (cmpt2 (λ x0 x1 . con0) (λ x0 x1 . con0) (λ x0 x1 . cmpt (λ x2 . crab (λ x3 . wbr (cv x3) c0 cfsupp) (λ x3 . co (cv x0) (cv x1) cmap)) (λ x2 . csb (coi (co (cv x2) c0 csupp) cep) (λ x3 . cfv (cdm (cv x3)) (cseqom (cmpt2 (λ x4 x5 . cvv) (λ x4 x5 . cvv) (λ x4 x5 . co (co (co (cv x0) (cfv (cv x4) (cv x3)) coe) (cfv (cfv (cv x4) (cv x3)) (cv x2)) comu) (cv x5) coa)) c0))))) (proof)
Theorem df_tc : wceq ctc (cmpt (λ x0 . cvv) (λ x0 . cint (cab (λ x1 . wa (wss (cv x0) (cv x1)) (wtr (cv x1)))))) (proof)
Theorem df_r1 : wceq cr1 (crdg (cmpt (λ x0 . cvv) (λ x0 . cpw (cv x0))) c0) (proof)
Theorem df_rank : wceq crnk (cmpt (λ x0 . cvv) (λ x0 . cint (crab (λ x1 . wcel (cv x0) (cfv (csuc (cv x1)) cr1)) (λ x1 . con0)))) (proof)
Theorem df_card : wceq ccrd (cmpt (λ x0 . cvv) (λ x0 . cint (crab (λ x1 . wbr (cv x1) (cv x0) cen) (λ x1 . con0)))) (proof)
Theorem df_aleph : wceq cale (crdg char com) (proof)
Theorem df_cf : wceq ccf (cmpt (λ x0 . con0) (λ x0 . cint (cab (λ x1 . wex (λ x2 . wa (wceq (cv x1) (cfv (cv x2) ccrd)) (wa (wss (cv x2) (cv x0)) (wral (λ x3 . wrex (λ x4 . wss (cv x3) (cv x4)) (λ x4 . cv x2)) (λ x3 . cv x0)))))))) (proof)
Theorem df_acn : ∀ x0 : ι → ο . wceq (wacn x0) (cab (λ x1 . wa (wcel x0 cvv) (wral (λ x2 . wex (λ x3 . wral (λ x4 . wcel (cfv (cv x4) (cv x3)) (cfv (cv x4) (cv x2))) (λ x4 . x0))) (λ x2 . co (cdif (cpw (cv x1)) (csn c0)) x0 cmap)))) (proof)
Theorem df_ac : wb wac (∀ x0 . wex (λ x1 . wa (wss (cv x1) (cv x0)) (wfn (cv x1) (cdm (cv x0))))) (proof)
Theorem df_cda : wceq ccda (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cun (cxp (cv x0) (csn c0)) (cxp (cv x1) (csn c1o)))) (proof)
Theorem df_fin1a : wceq cfin1a (cab (λ x0 . wral (λ x1 . wo (wcel (cv x1) cfn) (wcel (cdif (cv x0) (cv x1)) cfn)) (λ x1 . cpw (cv x0)))) (proof)
Theorem df_fin2 : wceq cfin2 (cab (λ x0 . wral (λ x1 . wa (wne (cv x1) c0) (wor (cv x1) crpss) ⟶ wcel (cuni (cv x1)) (cv x1)) (λ x1 . cpw (cpw (cv x0))))) (proof)
Theorem df_fin4 : wceq cfin4 (cab (λ x0 . wn (wex (λ x1 . wa (wpss (cv x1) (cv x0)) (wbr (cv x1) (cv x0) cen))))) (proof)
Theorem df_fin3 : wceq cfin3 (cab (λ x0 . wcel (cpw (cv x0)) cfin4)) (proof)
Theorem df_fin5 : wceq cfin5 (cab (λ x0 . wo (wceq (cv x0) c0) (wbr (cv x0) (co (cv x0) (cv x0) ccda) csdm))) (proof)
Theorem df_fin6 : wceq cfin6 (cab (λ x0 . wo (wbr (cv x0) c2o csdm) (wbr (cv x0) (cxp (cv x0) (cv x0)) csdm))) (proof)
Theorem df_fin7 : wceq cfin7 (cab (λ x0 . wn (wrex (λ x1 . wbr (cv x0) (cv x1) cen) (λ x1 . cdif con0 com)))) (proof)