Proofgold Address

Known ax_frege58b__ax_frege58b_b__df_bcc__df_addr__df_subr__df_mulv__df_ptdf__df_rr3__df_line3__df_vd1__df_vd2__df_vhc2__df_vhc3__df_vd3__df_liminf__df_xlim__df_salg__df_salon : ∀ x0 : ο . ((∀ x1 : ι → ο . ∀ x2 . (∀ x3 . x1 x3) ⟶ wsb x1 x2) ⟶ (∀ x1 : ι → ο . ∀ x2 . (∀ x3 . x1 x3) ⟶ wsb x1 x2) ⟶ wceq cbcc (cmpt2 (λ x1 x2 . cc) (λ x1 x2 . cn0) (λ x1 x2 . co (co (cv x1) (cv x2) cfallfac) (cfv (cv x2) cfa) cdiv)) ⟶ wceq cplusr (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cr) (λ x3 . co (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) caddc))) ⟶ wceq cminusr (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cr) (λ x3 . co (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) cmin))) ⟶ wceq ctimesr (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cr) (λ x3 . co (cv x1) (cfv (cv x3) (cv x2)) cmul))) ⟶ (∀ x1 x2 : ι → ο . wceq (cptdfc x1 x2) (cmpt (λ x3 . cr) (λ x3 . cima (co (co (cv x3) (co x2 x1 cminusr) ctimesr) x1 cpv) (ctp c1 c2 c3)))) ⟶ wceq crr3c (co cr (ctp c1 c2 c3) cmap) ⟶ wceq cline3 (crab (λ x1 . wa (wbr c2o (cv x1) cdom) (wral (λ x2 . wral (λ x3 . wne (cv x3) (cv x2) ⟶ wceq (crn (cptdfc (cv x2) (cv x3))) (cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1))) (λ x1 . cpw crr3c)) ⟶ (∀ x1 x2 : ο . wb (wvd1 x1 x2) (x1 ⟶ x2)) ⟶ (∀ x1 x2 x3 : ο . wb (wvd2 x1 x2 x3) (wa x1 x2 ⟶ x3)) ⟶ (∀ x1 x2 : ο . wb (wvhc2 x1 x2) (wa x1 x2)) ⟶ (∀ x1 x2 x3 : ο . wb (wvhc3 x1 x2 x3) (w3a x1 x2 x3)) ⟶ (∀ x1 x2 x3 x4 : ο . wb (wvd3 x1 x2 x3 x4) (w3a x1 x2 x3 ⟶ x4)) ⟶ wceq clsi (cmpt (λ x1 . cvv) (λ x1 . csup (crn (cmpt (λ x2 . cr) (λ x2 . cinf (cin (cima (cv x1) (co (cv x2) cpnf cico)) cxr) cxr clt))) cxr clt)) ⟶ wceq clsxlim (cfv (cfv cle cordt) clm) ⟶ wceq csalg (cab (λ x1 . w3a (wcel c0 (cv x1)) (wral (λ x2 . wcel (cdif (cuni (cv x1)) (cv x2)) (cv x1)) (λ x2 . cv x1)) (wral (λ x2 . wbr (cv x2) com cdom ⟶ wcel (cuni (cv x2)) (cv x1)) (λ x2 . cpw (cv x1))))) ⟶ wceq csalon (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wceq (cuni (cv x2)) (cv x1)) (λ x2 . csalg))) ⟶ x0) ⟶ x0
Theorem ax_frege58b_b : ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2) ⟶ wsb x0 x1 (proof)
Theorem ax_frege58b_b : ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2) ⟶ wsb x0 x1 (proof)
Theorem df_bcc : wceq cbcc (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cn0) (λ x0 x1 . co (co (cv x0) (cv x1) cfallfac) (cfv (cv x1) cfa) cdiv)) (proof)
Theorem df_addr : wceq cplusr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cr) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) caddc))) (proof)
Theorem df_subr : wceq cminusr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cr) (λ x2 . co (cfv (cv x2) (cv x0)) (cfv (cv x2) (cv x1)) cmin))) (proof)
Theorem df_mulv : wceq ctimesr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cr) (λ x2 . co (cv x0) (cfv (cv x2) (cv x1)) cmul))) (proof)
Theorem df_ptdf : ∀ x0 x1 : ι → ο . wceq (cptdfc x0 x1) (cmpt (λ x2 . cr) (λ x2 . cima (co (co (cv x2) (co x1 x0 cminusr) ctimesr) x0 cpv) (ctp c1 c2 c3))) (proof)
Theorem df_rr3 : wceq crr3c (co cr (ctp c1 c2 c3) cmap) (proof)
Theorem df_line3 : wceq cline3 (crab (λ x0 . wa (wbr c2o (cv x0) cdom) (wral (λ x1 . wral (λ x2 . wne (cv x2) (cv x1) ⟶ wceq (crn (cptdfc (cv x1) (cv x2))) (cv x0)) (λ x2 . cv x0)) (λ x1 . cv x0))) (λ x0 . cpw crr3c)) (proof)
Theorem df_vd1 : ∀ x0 x1 : ο . wb (wvd1 x0 x1) (x0 ⟶ x1) (proof)
Theorem df_vd2 : ∀ x0 x1 x2 : ο . wb (wvd2 x0 x1 x2) (wa x0 x1 ⟶ x2) (proof)
Theorem df_vhc2 : ∀ x0 x1 : ο . wb (wvhc2 x0 x1) (wa x0 x1) (proof)
Theorem df_vhc3 : ∀ x0 x1 x2 : ο . wb (wvhc3 x0 x1 x2) (w3a x0 x1 x2) (proof)
Theorem df_vd3 : ∀ x0 x1 x2 x3 : ο . wb (wvd3 x0 x1 x2 x3) (w3a x0 x1 x2 ⟶ x3) (proof)
Theorem df_liminf : wceq clsi (cmpt (λ x0 . cvv) (λ x0 . csup (crn (cmpt (λ x1 . cr) (λ x1 . cinf (cin (cima (cv x0) (co (cv x1) cpnf cico)) cxr) cxr clt))) cxr clt)) (proof)
Theorem df_xlim : wceq clsxlim (cfv (cfv cle cordt) clm) (proof)
Theorem df_salg : wceq csalg (cab (λ x0 . w3a (wcel c0 (cv x0)) (wral (λ x1 . wcel (cdif (cuni (cv x0)) (cv x1)) (cv x0)) (λ x1 . cv x0)) (wral (λ x1 . wbr (cv x1) com cdom ⟶ wcel (cuni (cv x1)) (cv x0)) (λ x1 . cpw (cv x0))))) (proof)
Theorem df_salon : wceq csalon (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wceq (cuni (cv x1)) (cv x0)) (λ x1 . csalg))) (proof)