Proofgold Address

Known b3824..^set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Theorem 535f2..^set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ x0 = x1 (proof)
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
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 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1
Known 4cb75..^Eps_i_R : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (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 : ο . x0 ⟶ or x0 x1
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or 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 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 22cc3.. : ∀ x0 : ο . ∀ x1 x2 . ∀ x3 : ο . (x0 ⟶ If_i x0 x1 x2 = x1 ⟶ x3) ⟶ (not x0 ⟶ If_i x0 x1 x2 = x2 ⟶ x3) ⟶ x3 (proof)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 81513..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2 (proof)
Theorem 0d2f9..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_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) ⟶ (x0 ⟶ not (x1 = x3) ⟶ False) ⟶ (not x0 ⟶ not (x2 = x3) ⟶ False) ⟶ False (proof)
Theorem bafdb..^tab_If_i_rhs : ∀ x0 : ο . ∀ x1 x2 x3 . not (x3 = If_i x0 x1 x2) ⟶ (x0 ⟶ not (x3 = x1) ⟶ False) ⟶ (not x0 ⟶ not (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 x1 ⟶ x1
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 = x1 ⟶ x3) ⟶ (x0 = x2 ⟶ x3) ⟶ x3 (proof)
Known f2c89..^{Empty_In_Power} : ∀ x0 . In 0 (Power x0)
Known f1bf4..^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ In (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 0 ⟶ False
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 = x0 ⟶ False) ⟶ (x2 = x1 ⟶ False) ⟶ False (proof)
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
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 = x0 ⟶ False) ⟶ 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 x2 ⟶ In x2 x0 ⟶ In x1 (Union x0)
Theorem 0ce8c..^binunionI1 : ∀ x0 x1 x2 . In x2 x0 ⟶ In x2 (binunion x0 x1) (proof)
Theorem eb8b4..^binunionI2 : ∀ x0 x1 x2 . In x2 x1 ⟶ In x2 (binunion x0 x1) (proof)
Known 2109a..^UnionE2 : ∀ x0 x1 . In x1 (Union x0) ⟶ ∀ x2 : ο . (∀ x3 . In x1 x3 ⟶ In x3 x0 ⟶ x2) ⟶ 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 x0 ⟶ x3) ⟶ (In x2 x1 ⟶ x3) ⟶ x3 (proof)
Theorem 1a63b..^{tab_pos_binunion} : ∀ x0 x1 x2 . In x2 (binunion x0 x1) ⟶ (In x2 x0 ⟶ False) ⟶ (In x2 x1 ⟶ False) ⟶ False (proof)
Known 9d2e6..^nIn_I2 : ∀ x0 x1 . (In x0 x1 ⟶ False) ⟶ nIn x0 x1
Theorem 1954c..^{tab_neg_binunion} : ∀ x0 x1 x2 . nIn x2 (binunion x0 x1) ⟶ (nIn x2 x0 ⟶ nIn x2 x1 ⟶ False) ⟶ False (proof)
Known d6778..^{Empty_Subq_eq} : ∀ x0 . Subq x0 0 ⟶ x0 = 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 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ 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 x0 ⟶ In 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 x0 ⟶ In 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 x0 ⟶ In x2 (x1 x3) ⟶ False) ⟶ False (proof)
Known 085e3..^contra_In : ∀ x0 x1 . (nIn x0 x1 ⟶ False) ⟶ In x0 x1
Theorem e3f8b..^{tab_neg_famunion} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . nIn x2 (famunion x0 x1) ⟶ (nIn x3 x0 ⟶ False) ⟶ (nIn x2 (x1 x3) ⟶ False) ⟶ False (proof)