Proofgold Address

Known df_op__df_ot__df_uni__df_int__df_iun__df_iin__df_disj__df_br__df_opab__df_opab_b__df_mpt__df_tr__ax_rep__ax_pow__df_id__df_eprel__df_po__df_so : ∀ x0 : ο . ((∀ x1 x2 : ι → ο . wceq (cop x1 x2) (cab (λ x3 . w3a (wcel x1 cvv) (wcel x2 cvv) (wcel (cv x3) (cpr (csn x1) (cpr x1 x2)))))) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (cotp x1 x2 x3) (cop (cop x1 x2) x3)) ⟶ (∀ x1 : ι → ο . wceq (cuni x1) (cab (λ x2 . wex (λ x3 . wa (wcel (cv x2) (cv x3)) (wcel (cv x3) x1))))) ⟶ (∀ x1 : ι → ο . wceq (cint x1) (cab (λ x2 . ∀ x3 . wcel (cv x3) x1 ⟶ wcel (cv x2) (cv x3)))) ⟶ (∀ x1 x2 : ι → ι → ο . wceq (ciun x1 x2) (cab (λ x3 . wrex (λ x4 . wcel (cv x3) (x2 x4)) x1))) ⟶ (∀ x1 x2 : ι → ι → ο . wceq (ciin x1 x2) (cab (λ x3 . wral (λ x4 . wcel (cv x3) (x2 x4)) x1))) ⟶ (∀ x1 x2 : ι → ι → ο . wb (wdisj x1 x2) (∀ x3 . wrmo (λ x4 . wcel (cv x3) (x2 x4)) x1)) ⟶ (∀ x1 x2 x3 : ι → ο . wb (wbr x1 x2 x3) (wcel (cop x1 x2) x3)) ⟶ (∀ x1 : ι → ι → ο . wceq (copab x1) (cab (λ x2 . wex (λ x3 . wex (λ x4 . wa (wceq (cv x2) (cop (cv x3) (cv x4))) (x1 x3 x4)))))) ⟶ (∀ x1 : ι → ο . wceq (copab_b x1) (cab (λ x2 . wex (λ x3 . wex (λ x4 . wa (wceq (cv x2) (cop (cv x4) (cv x4))) (x1 x4)))))) ⟶ (∀ x1 x2 : ι → ι → ο . wceq (cmpt x1 x2) (copab (λ x3 x4 . wa (wcel (cv x3) (x1 x3)) (wceq (cv x4) (x2 x3))))) ⟶ (∀ x1 : ι → ο . wb (wtr x1) (wss (cuni x1) x1)) ⟶ (∀ x1 : ι → ι → ι → ο . ∀ x2 . (∀ x3 . wex (λ x4 . ∀ x5 . (∀ x6 . x1 x6 x5 x3) ⟶ wceq (cv x5) (cv x4))) ⟶ wex (λ x3 . ∀ x4 . wb (wcel (cv x4) (cv x3)) (wex (λ x5 . wa (wcel (cv x5) (cv x2)) (∀ x6 . x1 x6 x4 x5))))) ⟶ (∀ x1 . wex (λ x2 . ∀ x3 . (∀ x4 . wcel (cv x4) (cv x3) ⟶ wcel (cv x4) (cv x1)) ⟶ wcel (cv x3) (cv x2))) ⟶ wceq cid (copab (λ x1 x2 . wceq (cv x1) (cv x2))) ⟶ wceq cep (copab (λ x1 x2 . wcel (cv x1) (cv x2))) ⟶ (∀ x1 x2 : ι → ο . wb (wpo x1 x2) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wa (wn (wbr (cv x3) (cv x3) x2)) (wa (wbr (cv x3) (cv x4) x2) (wbr (cv x4) (cv x5) x2) ⟶ wbr (cv x3) (cv x5) x2)) (λ x5 . x1)) (λ x4 . x1)) (λ x3 . x1))) ⟶ (∀ x1 x2 : ι → ο . wb (wor x1 x2) (wa (wpo x1 x2) (wral (λ x3 . wral (λ x4 . w3o (wbr (cv x3) (cv x4) x2) (wceq (cv x3) (cv x4)) (wbr (cv x4) (cv x3) x2)) (λ x4 . x1)) (λ x3 . x1)))) ⟶ x0) ⟶ x0
Theorem df_op : ∀ x0 x1 : ι → ο . wceq (cop x0 x1) (cab (λ x2 . w3a (wcel x0 cvv) (wcel x1 cvv) (wcel (cv x2) (cpr (csn x0) (cpr x0 x1))))) (proof)
Theorem df_ot : ∀ x0 x1 x2 : ι → ο . wceq (cotp x0 x1 x2) (cop (cop x0 x1) x2) (proof)
Theorem df_uni : ∀ x0 : ι → ο . wceq (cuni x0) (cab (λ x1 . wex (λ x2 . wa (wcel (cv x1) (cv x2)) (wcel (cv x2) x0)))) (proof)
Theorem df_int : ∀ x0 : ι → ο . wceq (cint x0) (cab (λ x1 . ∀ x2 . wcel (cv x2) x0 ⟶ wcel (cv x1) (cv x2))) (proof)
Theorem df_iun : ∀ x0 x1 : ι → ι → ο . wceq (ciun x0 x1) (cab (λ x2 . wrex (λ x3 . wcel (cv x2) (x1 x3)) x0)) (proof)
Theorem df_iin : ∀ x0 x1 : ι → ι → ο . wceq (ciin x0 x1) (cab (λ x2 . wral (λ x3 . wcel (cv x2) (x1 x3)) x0)) (proof)
Theorem df_disj : ∀ x0 x1 : ι → ι → ο . wb (wdisj x0 x1) (∀ x2 . wrmo (λ x3 . wcel (cv x2) (x1 x3)) x0) (proof)
Theorem df_br : ∀ x0 x1 x2 : ι → ο . wb (wbr x0 x1 x2) (wcel (cop x0 x1) x2) (proof)
Theorem df_opab : ∀ x0 : ι → ι → ο . wceq (copab x0) (cab (λ x1 . wex (λ x2 . wex (λ x3 . wa (wceq (cv x1) (cop (cv x2) (cv x3))) (x0 x2 x3))))) (proof)
Theorem df_opab_b : ∀ x0 : ι → ο . wceq (copab_b x0) (cab (λ x1 . wex (λ x2 . wex (λ x3 . wa (wceq (cv x1) (cop (cv x3) (cv x3))) (x0 x3))))) (proof)
Theorem df_mpt : ∀ x0 x1 : ι → ι → ο . wceq (cmpt x0 x1) (copab (λ x2 x3 . wa (wcel (cv x2) (x0 x2)) (wceq (cv x3) (x1 x2)))) (proof)
Theorem df_tr : ∀ x0 : ι → ο . wb (wtr x0) (wss (cuni x0) x0) (proof)
Theorem ax_rep : ∀ x0 : ι → ι → ι → ο . ∀ x1 . (∀ x2 . wex (λ x3 . ∀ x4 . (∀ x5 . x0 x5 x4 x2) ⟶ wceq (cv x4) (cv x3))) ⟶ wex (λ x2 . ∀ x3 . wb (wcel (cv x3) (cv x2)) (wex (λ x4 . wa (wcel (cv x4) (cv x1)) (∀ x5 . x0 x5 x3 x4)))) (proof)
Theorem ax_pow : ∀ x0 . wex (λ x1 . ∀ x2 . (∀ x3 . wcel (cv x3) (cv x2) ⟶ wcel (cv x3) (cv x0)) ⟶ wcel (cv x2) (cv x1)) (proof)
Theorem df_id : wceq cid (copab (λ x0 x1 . wceq (cv x0) (cv x1))) (proof)
Theorem df_eprel : wceq cep (copab (λ x0 x1 . wcel (cv x0) (cv x1))) (proof)
Theorem df_po : ∀ x0 x1 : ι → ο . wb (wpo x0 x1) (wral (λ x2 . wral (λ x3 . wral (λ x4 . wa (wn (wbr (cv x2) (cv x2) x1)) (wa (wbr (cv x2) (cv x3) x1) (wbr (cv x3) (cv x4) x1) ⟶ wbr (cv x2) (cv x4) x1)) (λ x4 . x0)) (λ x3 . x0)) (λ x2 . x0)) (proof)
Theorem df_so : ∀ x0 x1 : ι → ο . wb (wor x0 x1) (wa (wpo x0 x1) (wral (λ x2 . wral (λ x3 . w3o (wbr (cv x2) (cv x3) x1) (wceq (cv x2) (cv x3)) (wbr (cv x3) (cv x2) x1)) (λ x3 . x0)) (λ x2 . x0))) (proof)