Search for blocks/addresses/...

Proofgold Proposition

∀ 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) x1wcel (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
type
prop
theory
SetMM
name
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
proof
PUV1k..
Megalodon
-
proofgold address
TMTb3..
creator
36224 PrCmT../08035..
owner
36224 PrCmT../08035..
term root
38bc5..