Proofgold Address

Definition False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ False
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 39854..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0 (proof)
Theorem eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1 (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 13bcd..^iff_def : iff = λ x1 x2 : ο . and (x1 ⟶ x2) (x2 ⟶ x1)
Theorem 9fc94.. : ∀ x0 x1 : ο . iff x0 x1 ⟶ and (x0 ⟶ x1) (x1 ⟶ x0) (proof)
Theorem 50594..^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1 (proof)
Theorem 93720..^iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0 (proof)
Known 32c82..^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem ad656.. : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x2) ⟶ x2 (proof)
Known c1173..^Subq_def : Subq = λ x1 x2 . ∀ x3 . In x3 x1 ⟶ In x3 x2
Theorem b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1 (proof)
Theorem 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1 (proof)
Theorem 6696a..^Subq_ref : ∀ x0 . Subq x0 x0 (proof)
Known 7f305..^EmptyAx : not (∀ x0 : ο . (∀ x1 . In x1 0 ⟶ x0) ⟶ x0)
Theorem 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False (proof)
Known da6c8..^PowerEq : ∀ x0 x1 . iff (In x1 (Power x0)) (Subq x1 x0)
Theorem 2d44a..^PowerI : ∀ x0 x1 . Subq x1 x0 ⟶ In x1 (Power x0) (proof)
Theorem ae89b..^PowerE : ∀ x0 x1 . In x1 (Power x0) ⟶ Subq x1 x0 (proof)
Theorem 7b5f8..^{Self_In_Power} : ∀ x0 . In x0 (Power x0) (proof)
Theorem 025eb.. : 0 = Power 0 ⟶ False (proof)
Theorem 204a5.. : (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . and (x6 = x1 (x1 x5 (x1 x7 (x1 (x1 (x1 (x1 x6 (x1 (x1 x5 (x1 x5 (x1 (x1 x5 (x1 (x4 x5) (x1 (x1 x7 (x1 x6 (x1 x6 x6))) x5))) (x1 (x4 (x1 (x1 (x4 x7) x5) (x1 x5 x5))) (x1 x6 (x1 x6 (x1 (x1 (x1 x5 (x1 (x1 x5 (x1 (x4 x6) x7)) (x4 (x1 x7 x5)))) x6) (x4 (x1 (x1 x7 (x1 x5 (x1 (x4 (x1 x5 x7)) x5))) (x1 (x1 (x1 x6 (x1 (x4 x5) x6)) x6) (x4 (x4 (x1 (x1 (x1 (x1 x5 (x1 (x1 x6 (x1 (x1 x7 x5) x7)) x6)) x7) (x1 x7 (x1 x5 x5))) x6))))))))))))) (x1 (x1 (x1 (x1 (x1 x6 (x1 x5 x5)) (x4 (x4 (x1 x7 (x4 (x4 (x1 x7 x5))))))) x5) x6) (x1 x6 x7)))) x5) x5) (x4 x6)))) (x1 (x1 (x4 (x1 (x4 (x1 (x1 (x1 (x1 x7 (x1 (x4 (x4 (x1 (x1 x5 x6) x7))) (x4 (x1 x5 x5)))) x5) (x4 x5)) (x1 (x1 (x1 (x1 (x1 x5 x7) (x4 (x4 (x4 x7)))) x7) x6) x5))) (x1 (x1 (x1 x6 x5) (x4 x6)) x6))) x7) x6)) (∃ x8 . x3 (x4 x5))) ⟶ False (proof)
Theorem 2b6c7.. : (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 x8 x9 . and (∀ x10 . x4 x9 = x10 ⟶ and (x2 x10) (x7 = x5 ⟶ and (∀ x11 . x9 = x8) (∃ x11 . x3 x10)) ⟶ ∃ x11 . x7 = x7) (not (x3 (x4 (x4 (x1 x7 x5))))) ⟶ x6 = x9) ⟶ False (proof)
Theorem 1c497.. : (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . x4 (x1 (x1 (x1 (x1 (x1 (x1 x6 x5) (x1 (x1 (x1 x6 x5) (x1 x7 (x1 (x1 (x1 x5 x5) (x1 (x1 (x1 (x1 x5 (x1 (x1 x6 (x1 x5 (x1 x5 x7))) x5)) x7) (x1 (x4 x6) x7)) (x1 (x1 (x1 (x1 x5 (x4 (x1 x7 x5))) (x1 x6 x6)) (x1 x6 (x1 x7 x5))) x5))) x7))) x5)) x6) (x1 x6 (x1 x5 (x1 (x1 (x4 x5) (x1 (x1 x6 x6) x6)) x5)))) (x4 (x4 x6))) x5) = x4 (x4 x7)) ⟶ False (proof)
Theorem d3bc2.. : (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . ∀ x8 : ο . (∀ x9 . and (x9 = x7) (x4 (x1 (x1 (x4 (x1 (x1 (x1 (x1 (x1 x5 x7) (x4 (x4 (x1 (x1 x7 x5) x7)))) (x1 (x1 x5 x5) (x1 (x4 x5) (x1 x7 (x1 (x4 x5) x9))))) x9) x9)) x5) (x4 x5)) = x6) ⟶ x8) ⟶ x8) ⟶ False (proof)