Proofgold Address

Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Known 13bcd..^iff_def : iff = λ x1 x2 : ο . and (x1 ⟶ x2) (x2 ⟶ x1)
Known 50594..^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1
Known 93720..^iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem cd5b6..^exandI_i : ∀ x0 x1 : ι → ο . ∀ x2 . x0 x2 ⟶ x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (x0 x4) (x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 61640..^exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Known c1173..^Subq_def : Subq = λ x1 x2 . ∀ x3 . In x3 x1 ⟶ In x3 x2
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Theorem e3c91..^tab_pos_Subq : ∀ x0 x1 . Subq x0 x1 ⟶ ((∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ False) ⟶ False (proof)
Theorem 71338..^tab_neg_Subq : ∀ x0 x1 . not (Subq x0 x1) ⟶ (not (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ False) ⟶ False (proof)
Known 5f38d..^TransSet_def : TransSet = λ x1 . ∀ x2 . In x2 x1 ⟶ Subq x2 x1
Theorem 79a81..^TransSetI : ∀ x0 . (∀ x1 . In x1 x0 ⟶ Subq x1 x0) ⟶ TransSet x0 (proof)
Theorem 2fc4a..^TransSetE : ∀ x0 . TransSet x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq x1 x0 (proof)
Known 4705c..^atleast2_def : atleast2 = λ x1 . ∀ x2 : ο . (∀ x3 . and (In x3 x1) (not (Subq x1 (Power x3))) ⟶ x2) ⟶ x2
Theorem c2ced..^atleast2_I : ∀ x0 x1 . In x1 x0 ⟶ not (Subq x0 (Power x1)) ⟶ atleast2 x0 (proof)
Theorem ffa80..^atleast2_E : ∀ x0 . atleast2 x0 ⟶ ∀ x1 : ο . (∀ x2 . and (In x2 x0) (not (Subq x0 (Power x2))) ⟶ x1) ⟶ x1 (proof)
Known 98887..^atleast3_def : atleast3 = λ x1 . ∀ x2 : ο . (∀ x3 . and (Subq x3 x1) (and (not (Subq x1 x3)) (atleast2 x3)) ⟶ x2) ⟶ x2
Theorem 6b4a4..^atleast3_I : ∀ x0 x1 . Subq x1 x0 ⟶ not (Subq x0 x1) ⟶ atleast2 x1 ⟶ atleast3 x0 (proof)
Theorem 218d1..^atleast3_E : ∀ x0 . atleast3 x0 ⟶ ∀ x1 : ο . (∀ x2 . and (Subq x2 x0) (and (not (Subq x0 x2)) (atleast2 x2)) ⟶ x1) ⟶ x1 (proof)
Known d27ea..^atleast4_def : atleast4 = λ x1 . ∀ x2 : ο . (∀ x3 . and (Subq x3 x1) (and (not (Subq x1 x3)) (atleast3 x3)) ⟶ x2) ⟶ x2
Theorem 649d8..^atleast4_I : ∀ x0 x1 . Subq x1 x0 ⟶ not (Subq x0 x1) ⟶ atleast3 x1 ⟶ atleast4 x0 (proof)
Theorem 2dcf7..^atleast4_E : ∀ x0 . atleast4 x0 ⟶ ∀ x1 : ο . (∀ x2 . and (Subq x2 x0) (and (not (Subq x0 x2)) (atleast3 x2)) ⟶ x1) ⟶ x1 (proof)
Known 22d74..^atleast5_def : atleast5 = λ x1 . ∀ x2 : ο . (∀ x3 . and (Subq x3 x1) (and (not (Subq x1 x3)) (atleast4 x3)) ⟶ x2) ⟶ x2
Theorem 6ece7..^atleast5_I : ∀ x0 x1 . Subq x1 x0 ⟶ not (Subq x0 x1) ⟶ atleast4 x1 ⟶ atleast5 x0 (proof)
Theorem ee384..^atleast5_E : ∀ x0 . atleast5 x0 ⟶ ∀ x1 : ο . (∀ x2 . and (Subq x2 x0) (and (not (Subq x0 x2)) (atleast4 x2)) ⟶ x1) ⟶ x1 (proof)
Known 30e9c..^atleast6_def : atleast6 = λ x1 . ∀ x2 : ο . (∀ x3 . and (Subq x3 x1) (and (not (Subq x1 x3)) (atleast5 x3)) ⟶ x2) ⟶ x2
Theorem 500a3..^atleast6_I : ∀ x0 x1 . Subq x1 x0 ⟶ not (Subq x0 x1) ⟶ atleast5 x1 ⟶ atleast6 x0 (proof)
Theorem 5a74c..^atleast6_E : ∀ x0 . atleast6 x0 ⟶ ∀ x1 : ο . (∀ x2 . and (Subq x2 x0) (and (not (Subq x0 x2)) (atleast5 x2)) ⟶ x1) ⟶ x1 (proof)
Known 71a28..^exactly2_def : exactly2 = λ x1 . and (atleast2 x1) (not (atleast3 x1))
Theorem 0570d..^exactly2_I : ∀ x0 . atleast2 x0 ⟶ not (atleast3 x0) ⟶ exactly2 x0 (proof)
Theorem 84897..^exactly2_E : ∀ x0 . exactly2 x0 ⟶ and (atleast2 x0) (not (atleast3 x0)) (proof)
Known f9659..^exactly3_def : exactly3 = λ x1 . and (atleast3 x1) (not (atleast4 x1))
Theorem f2d7f..^exactly3_I : ∀ x0 . atleast3 x0 ⟶ not (atleast4 x0) ⟶ exactly3 x0 (proof)
Theorem 151e5..^exactly3_E : ∀ x0 . exactly3 x0 ⟶ and (atleast3 x0) (not (atleast4 x0)) (proof)
Known 5d30c..^exactly4_def : exactly4 = λ x1 . and (atleast4 x1) (not (atleast5 x1))
Theorem 3654c..^exactly4_I : ∀ x0 . atleast4 x0 ⟶ not (atleast5 x0) ⟶ exactly4 x0 (proof)
Theorem 01602..^exactly4_E : ∀ x0 . exactly4 x0 ⟶ and (atleast4 x0) (not (atleast5 x0)) (proof)
Known 50102..^exactly5_def : exactly5 = λ x1 . and (atleast5 x1) (not (atleast6 x1))
Theorem 15f81..^exactly5_I : ∀ x0 . atleast5 x0 ⟶ not (atleast6 x0) ⟶ exactly5 x0 (proof)
Theorem 2d4be..^exactly5_E : ∀ x0 . exactly5 x0 ⟶ and (atleast5 x0) (not (atleast6 x0)) (proof)
Known 382c5..^nIn_def : nIn = λ x1 x2 . not (In x1 x2)
Theorem 6abef..^nIn_I : ∀ x0 x1 . not (In x0 x1) ⟶ nIn x0 x1 (proof)
Theorem f0129..^nIn_E : ∀ x0 x1 . nIn x0 x1 ⟶ not (In x0 x1) (proof)
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Theorem 9d2e6..^nIn_I2 : ∀ x0 x1 . (In x0 x1 ⟶ False) ⟶ nIn x0 x1 (proof)
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False (proof)
Theorem 085e3..^contra_In : ∀ x0 x1 . (nIn x0 x1 ⟶ False) ⟶ In x0 x1 (proof)
Theorem ef881..^neg_nIn : ∀ x0 x1 . not (nIn x0 x1) ⟶ In x0 x1 (proof)
Known 557c1..^nSubq_def : nSubq = λ x1 x2 . not (Subq x1 x2)
Theorem bbed8..^nSubq_I : ∀ x0 x1 . not (Subq x0 x1) ⟶ nSubq x0 x1 (proof)
Theorem 3f1de..^nSubq_E : ∀ x0 x1 . nSubq x0 x1 ⟶ not (Subq x0 x1) (proof)
Theorem 579aa..^nSubq_I2 : ∀ x0 x1 . (Subq x0 x1 ⟶ False) ⟶ nSubq x0 x1 (proof)
Theorem b2a04..^nSubq_E2 : ∀ x0 x1 . nSubq x0 x1 ⟶ Subq x0 x1 ⟶ False (proof)
Theorem 80eaf..^neg_nSubq : ∀ x0 x1 . not (nSubq x0 x1) ⟶ Subq x0 x1 (proof)
Theorem a82da..^contra_Subq : ∀ x0 x1 . (nSubq x0 x1 ⟶ False) ⟶ Subq x0 x1 (proof)
Theorem 2ad64..^Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2 (proof)
Theorem a7ffa..^Subq_contra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ nIn x2 x1 ⟶ nIn x2 x0 (proof)
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Theorem 3cfc3..^nIn_Empty : ∀ x0 . nIn x0 0 (proof)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem b41a2..^Subq_Empty : ∀ x0 . Subq 0 x0 (proof)
Known b3824..^set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem d6778..^{Empty_Subq_eq} : ∀ x0 . Subq x0 0 ⟶ x0 = 0 (proof)
Theorem d0de4..^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0 (proof)
Known d182e..^iffE : ∀ x0 x1 : ο . iff x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ (not x0 ⟶ not x1 ⟶ x2) ⟶ x2
Known c7267..^UnionEq : ∀ x0 x1 . iff (In x1 (Union x0)) (∀ x2 : ο . (∀ x3 . and (In x1 x3) (In x3 x0) ⟶ x2) ⟶ x2)
Theorem ce145..^UnionE : ∀ x0 x1 . In x1 (Union x0) ⟶ ∀ x2 : ο . (∀ x3 . and (In x1 x3) (In x3 x0) ⟶ x2) ⟶ x2 (proof)
Theorem 2109a..^UnionE2 : ∀ x0 x1 . In x1 (Union x0) ⟶ ∀ x2 : ο . (∀ x3 . In x1 x3 ⟶ In x3 x0 ⟶ x2) ⟶ x2 (proof)
Theorem a4d26..^UnionI : ∀ x0 x1 x2 . In x1 x2 ⟶ In x2 x0 ⟶ In x1 (Union x0) (proof)
Theorem eb828..^{tab_pos_Union} : ∀ x0 x1 . In x1 (Union x0) ⟶ (∀ x2 . In x1 x2 ⟶ In x2 x0 ⟶ False) ⟶ False (proof)
Theorem f20e6..^{tab_neg_Union} : ∀ x0 x1 x2 . nIn x1 (Union x0) ⟶ (nIn x1 x2 ⟶ False) ⟶ (nIn x2 x0 ⟶ False) ⟶ False (proof)
Theorem fcac9..^Union_Empty : Union 0 = 0 (proof)
Known ae89b..^PowerE : ∀ x0 x1 . In x1 (Power x0) ⟶ Subq x1 x0
Known 2d44a..^PowerI : ∀ x0 x1 . Subq x1 x0 ⟶ In x1 (Power x0)
Theorem a71e8..^{tab_pos_Power} : ∀ x0 x1 . In x1 (Power x0) ⟶ (Subq x1 x0 ⟶ False) ⟶ False (proof)
Theorem cd88a..^{tab_neg_Power} : ∀ x0 x1 . nIn x1 (Power x0) ⟶ (nSubq x1 x0 ⟶ False) ⟶ False (proof)
Theorem f2c89..^{Empty_In_Power} : ∀ x0 . In 0 (Power x0) (proof)
Known 0d4e6..^ReplEq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (In x2 (Repl x0 x1)) (∀ x3 : ο . (∀ x4 . and (In x4 x0) (x2 = x1 x4) ⟶ x3) ⟶ x3)
Theorem 74a75..^ReplE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (In x4 x0) (x2 = x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 0f096..^ReplE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3 (proof)
Theorem f1bf4..^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ In (x1 x2) (Repl x0 x1) (proof)
Theorem c703f..^tab_pos_Repl : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1) ⟶ (∀ x3 . In x3 x0 ⟶ x2 = x1 x3 ⟶ False) ⟶ False (proof)
Theorem b0098..^tab_neg_Repl : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . nIn x2 (Repl x0 x1) ⟶ (nIn x3 x0 ⟶ False) ⟶ (not (x2 = x1 x3) ⟶ False) ⟶ False (proof)
Theorem 8a1cd..^Repl_Empty : ∀ x0 : ι → ι . Repl 0 x0 = 0 (proof)
Theorem 5a1ea..^{ReplEq_ext_sub} : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Subq (Repl x0 x1) (Repl x0 x2) (proof)
Theorem 09697..^ReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Repl x0 x1 = Repl x0 x2 (proof)