Proofgold Address

Known 0610a..^{neq_ordsucc_0} : ∀ x0 . not (ordsucc x0 = 0)
Theorem 97f79..^neq_3_0 : not (3 = 0) (proof)
Known aaf17..^{ordsucc_inj_contra} : ∀ x0 x1 . not (x0 = x1) ⟶ not (ordsucc x0 = ordsucc x1)
Known db5d7..^neq_2_0 : not (2 = 0)
Theorem 28881..^neq_3_1 : not (3 = 1) (proof)
Known 56778..^neq_2_1 : not (2 = 1)
Theorem f1fc4..^neq_3_2 : not (3 = 2) (proof)
Theorem fc9ff..^neq_4_0 : not (4 = 0) (proof)
Theorem 34131..^neq_4_1 : not (4 = 1) (proof)
Theorem 547fc..^neq_4_2 : not (4 = 2) (proof)
Theorem bfbcc..^neq_4_3 : not (4 = 3) (proof)
Theorem 3d58e..^neq_5_0 : not (5 = 0) (proof)
Theorem 03b32..^neq_5_1 : not (5 = 1) (proof)
Theorem b24f1..^neq_5_2 : not (5 = 2) (proof)
Theorem ab3a6..^neq_5_3 : not (5 = 3) (proof)
Theorem 8140f..^neq_5_4 : not (5 = 4) (proof)
Theorem 4193c..^neq_6_0 : not (6 = 0) (proof)
Theorem 53f92..^neq_6_1 : not (6 = 1) (proof)
Theorem f4b9c..^neq_6_2 : not (6 = 2) (proof)
Theorem 96787..^neq_6_3 : not (6 = 3) (proof)
Theorem 2a680..^neq_6_4 : not (6 = 4) (proof)
Theorem 3a5c9..^neq_6_5 : not (6 = 5) (proof)
Theorem ca789..^neq_7_0 : not (7 = 0) (proof)
Theorem 6a87a..^neq_7_1 : not (7 = 1) (proof)
Theorem 46692..^neq_7_2 : not (7 = 2) (proof)
Theorem c0553..^neq_7_3 : not (7 = 3) (proof)
Theorem 21c2e..^neq_7_4 : not (7 = 4) (proof)
Theorem fdff8..^neq_7_5 : not (7 = 5) (proof)
Theorem 0a1a6..^neq_7_6 : not (7 = 6) (proof)
Theorem c1d23..^neq_8_0 : not (8 = 0) (proof)
Theorem 3fd1f..^neq_8_1 : not (8 = 1) (proof)
Theorem 0aafe..^neq_8_2 : not (8 = 2) (proof)
Theorem 4862b..^neq_8_3 : not (8 = 3) (proof)
Theorem e99bd..^neq_8_4 : not (8 = 4) (proof)
Theorem c7589..^neq_8_5 : not (8 = 5) (proof)
Theorem 85418..^neq_8_6 : not (8 = 6) (proof)
Theorem 0ff51..^neq_8_7 : not (8 = 7) (proof)
Theorem 71f93..^neq_9_0 : not (9 = 0) (proof)
Theorem d7575..^neq_9_1 : not (9 = 1) (proof)
Theorem 5076a..^neq_9_2 : not (9 = 2) (proof)
Theorem b56e1..^neq_9_3 : not (9 = 3) (proof)
Theorem 178d5..^neq_9_4 : not (9 = 4) (proof)
Theorem ff515..^neq_9_5 : not (9 = 5) (proof)
Theorem 59e77..^neq_9_6 : not (9 = 6) (proof)
Theorem ed67b..^neq_9_7 : not (9 = 7) (proof)
Theorem bb081..^neq_9_8 : not (9 = 8) (proof)
Known 5f38d..^TransSet_def : TransSet = λ x1 . ∀ x2 . In x2 x1 ⟶ Subq x2 x1
Known c1173..^Subq_def : Subq = λ x1 x2 . ∀ x3 . In x3 x1 ⟶ In x3 x2
Theorem 300ec..^TransSetIb : ∀ x0 . (∀ x1 . In x1 x0 ⟶ ∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ TransSet x0 (proof)
Theorem 6e976..^TransSetEb : ∀ x0 . TransSet x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . In x2 x1 ⟶ In x2 x0 (proof)
Known f40a4..^ordinal_def : ordinal = λ x1 . and (TransSet x1) (∀ x2 . In x2 x1 ⟶ TransSet x2)
Known 39854..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Theorem 339db..^{ordinal_TransSet} : ∀ x0 . ordinal x0 ⟶ TransSet x0 (proof)
Theorem 1cf88..^{ordinal_TransSet_b} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . In x2 x1 ⟶ In x2 x0 (proof)
Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem be3f3..^{ordinal_In_TransSet} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ TransSet x1 (proof)
Theorem f2b18..^{ordinal_In_TransSet_b} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . In x2 x1 ⟶ ∀ x3 . In x3 x2 ⟶ In x3 x1 (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Theorem f9053..^{ordinal_Empty} : ordinal 0 (proof)
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Theorem 14977..^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ ordinal x1 (proof)
Known 61ad0..^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem 68454..^ordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ordinal x1 ⟶ x0 x1 (proof)
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known f6404..^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 48a85..^{least_ordinal_ex} : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2) ⟶ x1) ⟶ x1) ⟶ ∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . In x3 x2 ⟶ not (x0 x3)) ⟶ x1) ⟶ x1 (proof)
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Known b4776..^{ordsuccE_impred} : ∀ x0 x1 . In x1 (ordsucc x0) ⟶ ∀ x2 : ο . (In x1 x0 ⟶ x2) ⟶ (x1 = x0 ⟶ x2) ⟶ x2
Known e9b50..^ordsuccI1b : ∀ x0 x1 . In x1 x0 ⟶ In x1 (ordsucc x0)
Theorem 97a90..^{TransSet_ordsucc} : ∀ x0 . TransSet x0 ⟶ TransSet (ordsucc x0) (proof)
Theorem 8f4aa..^{ordinal_ordsucc} : ∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0) (proof)
Known fed08..^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known 08dfe..^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known c7c31..^nat_1 : nat_p 1
Theorem c2b57..^ordinal_1 : ordinal 1 (proof)
Known 36841..^nat_2 : nat_p 2
Theorem a2c28..^ordinal_2 : ordinal 2 (proof)
Theorem 27c30..^{TransSet_ordsucc_In_Subq} : ∀ x0 . TransSet x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq (ordsucc x1) x0 (proof)
Theorem 26a5d..^{ordinal_ordsucc_In_Subq} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq (ordsucc x1) x0 (proof)
Known 3ab01..^xmcases_In : ∀ x0 x1 . ∀ x2 : ο . (In x0 x1 ⟶ x2) ⟶ (nIn x0 x1 ⟶ x2) ⟶ x2
Known cb243..^or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Known a4277..^or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Known 8aff3..^or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Known 535f2..^set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ x0 = x1
Known 8cb38..^or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Theorem 3fa8b..^{ordinal_trichotomy_or} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (In x0 x1) (x0 = x1)) (In x1 x0) (proof)
Theorem 42117..^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (In x0 x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (In x1 x0 ⟶ x2) ⟶ x2 (proof)
Known 6fb1f..^{tab_neg_exactly1of2} : ∀ x0 x1 : ο . not (exactly1of2 x0 x1) ⟶ (x0 ⟶ x1 ⟶ False) ⟶ (not x0 ⟶ not x1 ⟶ False) ⟶ False
Theorem c603f..^{exactly1of2_I1} : ∀ x0 x1 : ο . x0 ⟶ not x1 ⟶ exactly1of2 x0 x1 (proof)
Theorem e4955..^{exactly1of2_I2} : ∀ x0 x1 : ο . not x0 ⟶ x1 ⟶ exactly1of2 x0 x1 (proof)
Known 71e01..^{exactly1of3_def} : exactly1of3 = λ x1 x2 x3 : ο . or (and (exactly1of2 x1 x2) (not x3)) (and (and (not x1) (not x2)) x3)
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem d04cf..^{exactly1of3_I1} : ∀ x0 x1 x2 : ο . x0 ⟶ not x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2 (proof)
Theorem 7eee1..^{exactly1of3_I2} : ∀ x0 x1 x2 : ο . not x0 ⟶ x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2 (proof)
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem 351d2..^{exactly1of3_I3} : ∀ x0 x1 x2 : ο . not x0 ⟶ not x1 ⟶ x2 ⟶ exactly1of3 x0 x1 x2 (proof)
Known e85f6..^In_irref : ∀ x0 . nIn x0 x0
Known 0f73a..^In_no2cycle : ∀ x0 x1 . In x0 x1 ⟶ In x1 x0 ⟶ False
Known 382c5..^nIn_def : nIn = λ x1 x2 . not (In x1 x2)
Theorem ed131..^{ordinal_trichotomy} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ exactly1of3 (In x0 x1) (x0 = x1) (In x1 x0) (proof)
Known 6696a..^Subq_ref : ∀ x0 . Subq x0 x0
Theorem 3e9a7..^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (In x0 x1) (Subq x1 x0) (proof)
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem a9fff..^{ordinal_linear} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (Subq x0 x1) (Subq x1 x0) (proof)
Theorem b651e..^{ordinal_ordsucc_In_eq} : ∀ x0 x1 . ordinal x0 ⟶ In x1 x0 ⟶ or (In (ordsucc x1) x0) (x0 = ordsucc x1) (proof)
Known 47706..^xmcases : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1
Theorem adbfc..^{ordinal_lim_or_succ} : ∀ x0 . ordinal x0 ⟶ or (∀ x1 . In x1 x0 ⟶ In (ordsucc x1) x0) (∀ x1 : ο . (∀ x2 . and (In x2 x0) (x0 = ordsucc x2) ⟶ x1) ⟶ x1) (proof)
Known 165f2..^ordsuccI1 : ∀ x0 . Subq x0 (ordsucc x0)
Known cf025..^ordsuccI2 : ∀ x0 . In x0 (ordsucc x0)
Known b3824..^set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem 6bb04..^{ordinal_ordsucc_In} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ In (ordsucc x1) (ordsucc x0) (proof)
Known 79a81..^TransSetI : ∀ x0 . (∀ x1 . In x1 x0 ⟶ Subq x1 x0) ⟶ TransSet x0
Known 2109a..^UnionE2 : ∀ x0 x1 . In x1 (Union x0) ⟶ ∀ x2 : ο . (∀ x3 . In x1 x3 ⟶ In x3 x0 ⟶ x2) ⟶ x2
Known a4d26..^UnionI : ∀ x0 x1 x2 . In x1 x2 ⟶ In x2 x0 ⟶ In x1 (Union x0)
Known 2fc4a..^TransSetE : ∀ x0 . TransSet x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq x1 x0
Theorem 19db8..^{ordinal_Union} : ∀ x0 . (∀ x1 . In x1 x0 ⟶ ordinal x1) ⟶ ordinal (Union x0) (proof)
Known 7b31d..^famunionE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (famunion x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ In x2 (x1 x4) ⟶ x3) ⟶ x3
Known 8f8c2..^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . In x2 x0 ⟶ In x3 (x1 x2) ⟶ In x3 (famunion x0 x1)
Theorem d7246..^{ordinal_famunion} : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . In x2 x0 ⟶ ordinal (x1 x2)) ⟶ ordinal (famunion x0 x1) (proof)
Known 485cd..^{binintersect_Subq_eq_1} : ∀ x0 x1 . Subq x0 x1 ⟶ binintersect x0 x1 = x0
Known 6b560..^{binintersect_com} : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0
Theorem 4ebb9..^{ordinal_binintersect} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (binintersect x0 x1) (proof)
Known 69c3f..^{Subq_binunion_eq} : ∀ x0 x1 . Subq x0 x1 = (binunion x0 x1 = x1)
Known 78b78..^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Theorem 78603..^{ordinal_binunion} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (binunion x0 x1) (proof)
Known aa3f4..^SepE_impred : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x1 x2 ⟶ x3) ⟶ x3
Known dab1f..^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 x0 ⟶ x1 x2 ⟶ In x2 (Sep x0 x1)
Known c4260..^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ In x2 x0
Theorem 62f91..^ordinal_Sep : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x2 ⟶ x1 x2 ⟶ x1 x3) ⟶ ordinal (Sep x0 x1) (proof)