Search for blocks/addresses/...

Proofgold Address

address
PUZD6BZw2zKErmvsTxdUdNCLYsNYo6WYcTJ
total
0
mg
-
conjpub
-
current assets
3baf4../66493.. bday: 36376 doc published by PrCmT..
Known df_coels__df_rels__df_ssr__df_refs__df_refrels__df_refrel__df_cnvrefs__df_cnvrefrels__df_cnvrefrel__df_syms__df_symrels__df_symrel__df_prt__ax_c5__ax_c4__ax_c7__ax_c10__ax_c10_b : ∀ x0 : ο . ((∀ x1 : ι → ο . wceq (ccoels x1) (ccoss (cres (ccnv cep) x1)))wceq crels (cpw (cxp cvv cvv))wceq cssr (copab (λ x1 x2 . wss (cv x1) (cv x2)))wceq crefs (cab (λ x1 . wbr (cin cid (cxp (cdm (cv x1)) (crn (cv x1)))) (cin (cv x1) (cxp (cdm (cv x1)) (crn (cv x1)))) cssr))wceq crefrels (cin crefs crels)(∀ x1 : ι → ο . wb (wrefrel x1) (wa (wss (cin cid (cxp (cdm x1) (crn x1))) (cin x1 (cxp (cdm x1) (crn x1)))) (wrel x1)))wceq ccnvrefs (cab (λ x1 . wbr (cin cid (cxp (cdm (cv x1)) (crn (cv x1)))) (cin (cv x1) (cxp (cdm (cv x1)) (crn (cv x1)))) (ccnv cssr)))wceq ccnvrefrels (cin ccnvrefs crels)(∀ x1 : ι → ο . wb (wcnvrefrel x1) (wa (wss (cin x1 (cxp (cdm x1) (crn x1))) (cin cid (cxp (cdm x1) (crn x1)))) (wrel x1)))wceq csyms (cab (λ x1 . wbr (ccnv (cin (cv x1) (cxp (cdm (cv x1)) (crn (cv x1))))) (cin (cv x1) (cxp (cdm (cv x1)) (crn (cv x1)))) cssr))wceq csymrels (cin csyms crels)(∀ x1 : ι → ο . wb (wsymrel x1) (wa (wss (ccnv (cin x1 (cxp (cdm x1) (crn x1)))) (cin x1 (cxp (cdm x1) (crn x1)))) (wrel x1)))(∀ x1 : ι → ο . wb (wprt x1) (wral (λ x2 . wral (λ x3 . wo (wceq (cv x2) (cv x3)) (wceq (cin (cv x2) (cv x3)) c0)) (λ x3 . x1)) (λ x2 . x1)))(∀ x1 : ι → ο . ∀ x2 . (∀ x3 . x1 x3)x1 x2)(∀ x1 x2 : ι → ο . (∀ x3 . (∀ x4 . x1 x4)x2 x3)(∀ x3 . x1 x3)∀ x3 . x2 x3)(∀ x1 : ι → ο . ∀ x2 . wn (∀ x3 . wn (∀ x4 . x1 x4))x1 x2)(∀ x1 : ι → ο . ∀ x2 x3 . (∀ x4 . wceq (cv x4) (cv x2)∀ x5 . x1 x5)x1 x3)(∀ x1 : ι → ο . ∀ x2 . (∀ x3 . wceq (cv x3) (cv x3)∀ x4 . x1 x4)x1 x2)x0)x0
Theorem df_coels : ∀ x0 : ι → ο . wceq (ccoels x0) (ccoss (cres (ccnv cep) x0)) (proof)
Theorem df_rels : wceq crels (cpw (cxp cvv cvv)) (proof)
Theorem df_ssr : wceq cssr (copab (λ x0 x1 . wss (cv x0) (cv x1))) (proof)
Theorem df_refs : wceq crefs (cab (λ x0 . wbr (cin cid (cxp (cdm (cv x0)) (crn (cv x0)))) (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0)))) cssr)) (proof)
Theorem df_refrels : wceq crefrels (cin crefs crels) (proof)
Theorem df_refrel : ∀ x0 : ι → ο . wb (wrefrel x0) (wa (wss (cin cid (cxp (cdm x0) (crn x0))) (cin x0 (cxp (cdm x0) (crn x0)))) (wrel x0)) (proof)
Theorem df_cnvrefs : wceq ccnvrefs (cab (λ x0 . wbr (cin cid (cxp (cdm (cv x0)) (crn (cv x0)))) (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0)))) (ccnv cssr))) (proof)
Theorem df_cnvrefrels : wceq ccnvrefrels (cin ccnvrefs crels) (proof)
Theorem df_cnvrefrel : ∀ x0 : ι → ο . wb (wcnvrefrel x0) (wa (wss (cin x0 (cxp (cdm x0) (crn x0))) (cin cid (cxp (cdm x0) (crn x0)))) (wrel x0)) (proof)
Theorem df_syms : wceq csyms (cab (λ x0 . wbr (ccnv (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0))))) (cin (cv x0) (cxp (cdm (cv x0)) (crn (cv x0)))) cssr)) (proof)
Theorem df_symrels : wceq csymrels (cin csyms crels) (proof)
Theorem df_symrel : ∀ x0 : ι → ο . wb (wsymrel x0) (wa (wss (ccnv (cin x0 (cxp (cdm x0) (crn x0)))) (cin x0 (cxp (cdm x0) (crn x0)))) (wrel x0)) (proof)
Theorem df_prt : ∀ x0 : ι → ο . wb (wprt x0) (wral (λ x1 . wral (λ x2 . wo (wceq (cv x1) (cv x2)) (wceq (cin (cv x1) (cv x2)) c0)) (λ x2 . x0)) (λ x1 . x0)) (proof)
Theorem ax_c5 : ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . x0 x2)x0 x1 (proof)
Theorem ax_c4 : ∀ x0 x1 : ι → ο . (∀ x2 . (∀ x3 . x0 x3)x1 x2)(∀ x2 . x0 x2)∀ x2 . x1 x2 (proof)
Theorem ax_c7 : ∀ x0 : ι → ο . ∀ x1 . wn (∀ x2 . wn (∀ x3 . x0 x3))x0 x1 (proof)
Theorem ax_c10 : ∀ x0 : ι → ο . ∀ x1 x2 . (∀ x3 . wceq (cv x3) (cv x1)∀ x4 . x0 x4)x0 x2 (proof)
Theorem ax_c10_b : ∀ x0 : ι → ο . ∀ x1 . (∀ x2 . wceq (cv x2) (cv x2)∀ x3 . x0 x3)x0 x1 (proof)

previous assets