Search for blocks/addresses/...

Proofgold Address

address
PUZ3GHjCEAN1TuZAYWwvRrYdTfQuTLPC6ki
total
0
mg
-
conjpub
-
current assets
bd8d3../8949f.. bday: 1339 doc published by PrGxv..
Known b3824..set_ext : ∀ x0 x1 . Subq x0 x1Subq x1 x0x0 = x1
Known b0dce..SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0In x2 x1)Subq x0 x1
Theorem 535f2..set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0In x2 x1)(∀ x2 . In x2 x1In x2 x0)x0 = x1 (proof)
Known 8106d..notI : ∀ x0 : ο . (x0False)not x0
Known notEnotE : ∀ x0 : ο . not x0x0False
Theorem 73fda..neq_sym_i : ∀ x0 x1 . not (x0 = x1)not (x1 = x0) (proof)
Theorem 3b206..tab_neq_i_sym : ∀ x0 x1 . not (x0 = x1)(not (x1 = x0)False)False (proof)
Known 47706..xmcases : ∀ x0 x1 : ο . (x0x1)(not x0x1)x1
Known 4cb75..Eps_i_R : ∀ x0 : ι → ο . ∀ x1 . x0 x1x0 (Eps_i x0)
Theorem 9c6aa..tab_Eps_i : ∀ x0 : ι → ο . ((∀ x1 . not (x0 x1))False)(x0 (Eps_i x0)False)False (proof)
Known bc395..If_i_def : If_i = λ x1 : ο . λ x2 x3 . Eps_i (λ x4 . or (and x1 (x4 = x2)) (and (not x1) (x4 = x3)))
Known dcbd9..orIL : ∀ x0 x1 : ο . x0or x0 x1
Known 7c02f..andI : ∀ x0 x1 : ο . x0x1and x0 x1
Known eca40..orIR : ∀ x0 x1 : ο . x1or x0 x1
Theorem 66ffc.. : ∀ x0 : ο . ∀ x1 x2 . or (and x0 (If_i x0 x1 x2 = x1)) (and (not x0) (If_i x0 x1 x2 = x2)) (proof)
Known 37124..orE : ∀ x0 x1 : ο . or x0 x1∀ x2 : ο . (x0x2)(x1x2)x2
Known andEandE : ∀ x0 x1 : ο . and x0 x1∀ x2 : ο . (x0x1x2)x2
Theorem 22cc3.. : ∀ x0 : ο . ∀ x1 x2 . ∀ x3 : ο . (x0If_i x0 x1 x2 = x1x3)(not x0If_i x0 x1 x2 = x2x3)x3 (proof)
Known FalseEFalseE : False∀ x0 : ο . x0
Theorem 81513..If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2 (proof)
Theorem 0d2f9..If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1 (proof)
Theorem e01bb..If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2) (proof)
Theorem d99e3..tab_If_i_lhs : ∀ x0 : ο . ∀ x1 x2 x3 . not (If_i x0 x1 x2 = x3)(x0not (x1 = x3)False)(not x0not (x2 = x3)False)False (proof)
Theorem bafdb..tab_If_i_rhs : ∀ x0 : ο . ∀ x1 x2 x3 . not (x3 = If_i x0 x1 x2)(x0not (x3 = x1)False)(not x0not (x3 = x2)False)False (proof)
Known 74a75..ReplE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1)∀ x3 : ο . (∀ x4 . and (In x4 x0) (x2 = x1 x4)x3)x3
Known c471b..UPair_def : UPair = λ x1 x2 . Repl (Power (Power 0)) (λ x3 . If_i (In 0 x3) x1 x2)
Known eb789..andER : ∀ x0 x1 : ο . and x0 x1x1
Theorem 469e5..UPairE : ∀ x0 x1 x2 . In x0 (UPair x1 x2)or (x0 = x1) (x0 = x2) (proof)
Theorem 7aad1..UPairE_cases : ∀ x0 x1 x2 . In x0 (UPair x1 x2)∀ x3 : ο . (x0 = x1x3)(x0 = x2x3)x3 (proof)
Known f2c89..Empty_In_Power : ∀ x0 . In 0 (Power x0)
Known f1bf4..ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0In (x1 x2) (Repl x0 x1)
Known 7b5f8..Self_In_Power : ∀ x0 . In x0 (Power x0)
Theorem 69fe1..UPairI1 : ∀ x0 x1 . In x0 (UPair x0 x1) (proof)
Known 2901c..EmptyE : ∀ x0 . In x0 0False
Theorem 7477d..UPairI2 : ∀ x0 x1 . In x1 (UPair x0 x1) (proof)
Theorem a441e.. : ∀ x0 x1 . Subq (UPair x0 x1) (UPair x1 x0) (proof)
Theorem a4584..UPair_com : ∀ x0 x1 . UPair x0 x1 = UPair x1 x0 (proof)
Theorem aa2ac..tab_pos_UPair : ∀ x0 x1 x2 . In x2 (UPair x0 x1)(x2 = x0False)(x2 = x1False)False (proof)
Known 24526..nIn_E2 : ∀ x0 x1 . nIn x0 x1In x0 x1False
Theorem 00e5e..tab_neg_UPair : ∀ x0 x1 x2 . nIn x2 (UPair x0 x1)(not (x2 = x0)not (x2 = x1)False)False (proof)
Known 58f30..Sing_def : Sing = λ x1 . UPair x1 x1
Theorem 1f15b..SingI : ∀ x0 . In x0 (Sing x0) (proof)
Theorem 9ae18..SingE : ∀ x0 x1 . In x1 (Sing x0)x1 = x0 (proof)
Theorem 5d18f..tab_pos_Sing : ∀ x0 x1 . In x1 (Sing x0)(x1 = x0False)False (proof)
Theorem 999dc..tab_neg_Sing : ∀ x0 x1 . nIn x1 (Sing x0)(not (x1 = x0)False)False (proof)
Known ba2d5..binunion_def : binunion = λ x1 x2 . Union (UPair x1 x2)
Known a4d26..UnionI : ∀ x0 x1 x2 . In x1 x2In x2 x0In x1 (Union x0)
Theorem 0ce8c..binunionI1 : ∀ x0 x1 x2 . In x2 x0In x2 (binunion x0 x1) (proof)
Theorem eb8b4..binunionI2 : ∀ x0 x1 x2 . In x2 x1In x2 (binunion x0 x1) (proof)
Known 2109a..UnionE2 : ∀ x0 x1 . In x1 (Union x0)∀ x2 : ο . (∀ x3 . In x1 x3In x3 x0x2)x2
Theorem e9b2c..binunionE : ∀ x0 x1 x2 . In x2 (binunion x0 x1)or (In x2 x0) (In x2 x1) (proof)
Theorem f9974..binunionE_cases : ∀ x0 x1 x2 . In x2 (binunion x0 x1)∀ x3 : ο . (In x2 x0x3)(In x2 x1x3)x3 (proof)
Theorem 1a63b..tab_pos_binunion : ∀ x0 x1 x2 . In x2 (binunion x0 x1)(In x2 x0False)(In x2 x1False)False (proof)
Known 9d2e6..nIn_I2 : ∀ x0 x1 . (In x0 x1False)nIn x0 x1
Theorem 1954c..tab_neg_binunion : ∀ x0 x1 x2 . nIn x2 (binunion x0 x1)(nIn x2 x0nIn x2 x1False)False (proof)
Known d6778..Empty_Subq_eq : ∀ x0 . Subq x0 0x0 = 0
Known ae89b..PowerE : ∀ x0 x1 . In x1 (Power x0)Subq x1 x0
Theorem 1b18d..Power_0_Sing_0 : Power 0 = Sing 0 (proof)
Known 0f096..ReplE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1)∀ x3 : ο . (∀ x4 . In x4 x0x2 = x1 x4x3)x3
Theorem 62bc0..Repl_UPair : ∀ x0 : ι → ι . ∀ x1 x2 . Repl (UPair x1 x2) x0 = UPair (x0 x1) (x0 x2) (proof)
Theorem 93e44..Repl_Sing : ∀ x0 : ι → ι . ∀ x1 . Repl (Sing x1) x0 = Sing (x0 x1) (proof)
Known d6d60..famunion_def : famunion = λ x1 . λ x2 : ι → ι . Union (Repl x1 x2)
Theorem 8f8c2..famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . In x2 x0In x3 (x1 x2)In x3 (famunion x0 x1) (proof)
Theorem 390bb..famunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (famunion x0 x1)∀ x3 : ο . (∀ x4 . and (In x4 x0) (In x2 (x1 x4))x3)x3 (proof)
Theorem 7b31d..famunionE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (famunion x0 x1)∀ x3 : ο . (∀ x4 . In x4 x0In x2 (x1 x4)x3)x3 (proof)
Theorem 40534..UnionEq_famunionId : ∀ x0 . Union x0 = famunion x0 (λ x2 . x2) (proof)
Theorem 1844d..ReplEq_famunion_Sing : ∀ x0 . ∀ x1 : ι → ι . Repl x0 x1 = famunion x0 (λ x3 . Sing (x1 x3)) (proof)
Theorem db4b2..tab_pos_famunion : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (famunion x0 x1)(∀ x3 . In x3 x0In x2 (x1 x3)False)False (proof)
Known 085e3..contra_In : ∀ x0 x1 . (nIn x0 x1False)In x0 x1
Theorem e3f8b..tab_neg_famunion : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . nIn x2 (famunion x0 x1)(nIn x3 x0False)(nIn x2 (x1 x3)False)False (proof)

previous assets