Proofgold Address

Theorem 15e97..^eq_sym_i : ∀ x0 x1 . x0 = x1 ⟶ x1 = x0
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)
Known 61ad0..^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Known 9d2e6..^nIn_I2 : ∀ x0 x1 . (In x0 x1 ⟶ False) ⟶ nIn x0 x1
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Theorem e85f6..^In_irref : ∀ x0 . nIn x0 x0
Theorem 0f73a..^In_no2cycle : ∀ x0 x1 . In x0 x1 ⟶ In x1 x0 ⟶ False
Theorem a0c6c..^In_no3cycle : ∀ x0 x1 x2 . In x0 x1 ⟶ In x1 x2 ⟶ In x2 x0 ⟶ False
Known c5eb1..^ordsucc_def : ordsucc = λ x1 . binunion x1 (Sing x1)
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Known 0ce8c..^binunionI1 : ∀ x0 x1 x2 . In x2 x0 ⟶ In x2 (binunion x0 x1)
Theorem 165f2..^ordsuccI1 : ∀ x0 . Subq x0 (ordsucc x0)
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Theorem e9b50..^ordsuccI1b : ∀ x0 x1 . In x1 x0 ⟶ In x1 (ordsucc x0)
Known eb8b4..^binunionI2 : ∀ x0 x1 x2 . In x2 x1 ⟶ In x2 (binunion x0 x1)
Known 1f15b..^SingI : ∀ x0 . In x0 (Sing x0)
Theorem cf025..^ordsuccI2 : ∀ x0 . In x0 (ordsucc x0)
Known f9974..^{binunionE_cases} : ∀ x0 x1 x2 . In x2 (binunion x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x3) ⟶ (In x2 x1 ⟶ x3) ⟶ x3
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known 9ae18..^SingE : ∀ x0 x1 . In x1 (Sing x0) ⟶ x1 = x0
Theorem 1373d..^ordsuccE : ∀ x0 x1 . In x1 (ordsucc x0) ⟶ or (In x1 x0) (x1 = x0)
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem b4776..^{ordsuccE_impred} : ∀ x0 x1 . In x1 (ordsucc x0) ⟶ ∀ x2 : ο . (In x1 x0 ⟶ x2) ⟶ (x1 = x0 ⟶ x2) ⟶ x2
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Theorem c985e..^{neq_0_ordsucc} : ∀ x0 . not (0 = ordsucc x0)
Theorem 0610a..^{neq_ordsucc_0} : ∀ x0 . not (ordsucc x0 = 0)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 74738..^ordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1 ⟶ x0 = x1
Theorem aaf17..^{ordsucc_inj_contra} : ∀ x0 x1 . not (x0 = x1) ⟶ not (ordsucc x0 = ordsucc x1)
Theorem 0978b..^In_0_1 : In 0 1
Theorem 0863e..^In_0_2 : In 0 2
Theorem 0a117..^In_1_2 : In 1 2
Theorem e51a8..^cases_1 : ∀ x0 . In x0 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Theorem 3ad28..^cases_2 : ∀ x0 . In x0 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Theorem 416bd..^cases_3 : ∀ x0 . In x0 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
Theorem 8b3d1..^cases_4 : ∀ x0 . In x0 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Theorem 2d26c..^cases_5 : ∀ x0 . In x0 5 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 x0
Theorem a05e0..^cases_6 : ∀ x0 . In x0 6 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 x0
Theorem 4d7f5..^cases_7 : ∀ x0 . In x0 7 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 6 ⟶ x1 x0
Theorem 8d7d3..^cases_8 : ∀ x0 . In x0 8 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 6 ⟶ x1 7 ⟶ x1 x0
Theorem 1414e..^cases_9 : ∀ x0 . In x0 9 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 6 ⟶ x1 7 ⟶ x1 8 ⟶ x1 x0
Theorem e3ec9..^neq_0_1 : not (0 = 1)
Theorem a871f..^neq_1_0 : not (1 = 0)
Theorem f043b..^neq_0_2 : not (0 = 2)
Theorem db5d7..^neq_2_0 : not (2 = 0)
Theorem 69ac1..^neq_1_2 : not (1 = 2)
Theorem 56778..^neq_2_1 : not (2 = 1)
Known b41a2..^Subq_Empty : ∀ x0 . Subq 0 x0
Theorem 25820..^Subq_0_0 : Subq 0 0
Theorem baaef..^Subq_0_1 : Subq 0 1
Theorem 22aa5..^Subq_0_2 : Subq 0 2
Known 6696a..^Subq_ref : ∀ x0 . Subq x0 x0
Theorem a95bd..^Subq_1_1 : Subq 1 1
Theorem a21f3..^Subq_1_2 : Subq 1 2
Theorem a9130..^Subq_2_2 : Subq 2 2
Theorem 830d8..^Subq_1_Sing0 : Subq 1 (Sing 0)
Theorem cdfbd..^Subq_Sing0_1 : Subq (Sing 0) 1
Known b3824..^set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem 5c344..^eq_1_Sing0 : 1 = Sing 0
Known 69fe1..^UPairI1 : ∀ x0 x1 . In x0 (UPair x0 x1)
Known 7477d..^UPairI2 : ∀ x0 x1 . In x1 (UPair x0 x1)
Theorem 8fa42..^{Subq_2_UPair01} : Subq 2 (UPair 0 1)
Known 7aad1..^UPairE_cases : ∀ x0 x1 x2 . In x0 (UPair x1 x2) ⟶ ∀ x3 : ο . (x0 = x1 ⟶ x3) ⟶ (x0 = x2 ⟶ x3) ⟶ x3
Theorem bdcc4..^{Subq_UPair01_2} : Subq (UPair 0 1) 2
Theorem fd6b1..^eq_2_UPair01 : 2 = UPair 0 1
Known de33e..^nat_p_def : nat_p = λ x1 . ∀ x2 : ι → ο . x2 0 ⟶ (∀ x3 . x2 x3 ⟶ x2 (ordsucc x3)) ⟶ x2 x1
Theorem 08405..^nat_0 : nat_p 0
Theorem 21479..^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem c7c31..^nat_1 : nat_p 1
Theorem 36841..^nat_2 : nat_p 2
Theorem 7bd16..^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ In 0 (ordsucc x0)
Theorem 840d1..^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ In (ordsucc x1) (ordsucc x0)
Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem fed08..^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Theorem c7246..^nat_inv : ∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∃ x1 . and (nat_p x1) (x0 = ordsucc x1))
Theorem 92870..^{nat_complete_ind} : ∀ x0 : ι → ο . (∀ x1 . nat_p x1 ⟶ (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Theorem b0a90..^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ nat_p x1
Known 2ad64..^Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Theorem 80da5..^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq x1 x0
Known 5f38d..^TransSet_def : TransSet = λ x1 . ∀ x2 . In x2 x1 ⟶ Subq x2 x1
Theorem 1358f..^nat_TransSet : ∀ x0 . nat_p x0 ⟶ TransSet x0
Known f40a4..^ordinal_def : ordinal = λ x1 . and (TransSet x1) (∀ x2 . In x2 x1 ⟶ TransSet x2)
Theorem 08dfe..^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Theorem 8cf6a..^{nat_ordsucc_trans} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 (ordsucc x0) ⟶ Subq x1 x0
Known 535f2..^set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ x0 = x1
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)
Theorem 48ae5..^{Union_ordsucc_eq} : ∀ x0 . nat_p x0 ⟶ Union (ordsucc x0) = x0
Theorem 82574..^In_0_3 : In 0 3
Theorem f0f3e..^In_1_3 : In 1 3
Theorem b5e95..^In_2_3 : In 2 3
Theorem 71a8d..^In_0_4 : In 0 4
Theorem efe66..^In_1_4 : In 1 4
Theorem 884f0..^In_2_4 : In 2 4
Theorem d9ca3..^In_3_4 : In 3 4
Theorem 5ec9a..^In_0_5 : In 0 5
Theorem 53692..^In_1_5 : In 1 5
Theorem 7f632..^In_2_5 : In 2 5
Theorem c3428..^In_3_5 : In 3 5
Theorem 55f57..^In_4_5 : In 4 5
Theorem 0f549..^In_0_6 : In 0 6
Theorem e5e7b..^In_1_6 : In 1 6
Theorem c6359..^In_2_6 : In 2 6
Theorem d5bd4..^In_3_6 : In 3 6
Theorem 99a7f..^In_4_6 : In 4 6
Theorem ad142..^In_5_6 : In 5 6
Theorem 6516d..^In_0_7 : In 0 7
Theorem ed9ed..^In_1_7 : In 1 7
Theorem e6c7c..^In_2_7 : In 2 7
Theorem dc43c..^In_3_7 : In 3 7
Theorem fb74e..^In_4_7 : In 4 7
Theorem 59629..^In_5_7 : In 5 7
Theorem 14a1c..^In_6_7 : In 6 7
Theorem 57d5b..^In_0_8 : In 0 8
Theorem 4c0a3..^In_1_8 : In 1 8
Theorem b8348..^In_2_8 : In 2 8
Theorem ace10..^In_3_8 : In 3 8
Theorem e08a8..^In_4_8 : In 4 8
Theorem 9ad9e..^In_5_8 : In 5 8
Theorem e821f..^In_6_8 : In 6 8
Theorem 879be..^In_7_8 : In 7 8
Theorem fda50..^In_0_9 : In 0 9
Theorem 9744a..^In_1_9 : In 1 9
Theorem 2df93..^In_2_9 : In 2 9
Theorem c585f..^In_3_9 : In 3 9
Theorem 8ee2c..^In_4_9 : In 4 9
Theorem e48d3..^In_5_9 : In 5 9
Theorem 35438..^In_6_9 : In 6 9
Theorem 3f605..^In_7_9 : In 7 9
Theorem dab47..^In_8_9 : In 8 9
Known 3cfc3..^nIn_Empty : ∀ x0 . nIn x0 0
Theorem 9dcaa..^nIn_0_0 : nIn 0 0
Theorem 18175..^nIn_1_0 : nIn 1 0
Theorem 7a610..^nIn_2_0 : nIn 2 0
Theorem 6e7db..^nIn_1_1 : nIn 1 1
Theorem 0ba24..^nIn_2_1 : nIn 2 1
Theorem df31d..^nIn_2_2 : nIn 2 2
Known 557c1..^nSubq_def : nSubq = λ x1 x2 . not (Subq x1 x2)
Theorem 16ddf..^nSubq_1_0 : nSubq 1 0
Theorem 23c6f..^nSubq_2_0 : nSubq 2 0
Theorem e21f2..^nSubq_2_1 : nSubq 2 1