Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-peano4 Structured version   GIF version

Theorem bj-peano4 7316
 Description: Remove from peano4 4243 dependency on ax-setind 4200. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)
Assertion
Ref Expression
bj-peano4 ((A 𝜔 B 𝜔) → (suc A = suc BA = B))

Proof of Theorem bj-peano4
StepHypRef Expression
1 3simpa 887 . . . . 5 ((A 𝜔 B 𝜔 suc A = suc B) → (A 𝜔 B 𝜔))
2 pm3.22 252 . . . . 5 ((A 𝜔 B 𝜔) → (B 𝜔 A 𝜔))
3 bj-nnen2lp 7315 . . . . 5 ((B 𝜔 A 𝜔) → ¬ (B A A B))
41, 2, 33syl 17 . . . 4 ((A 𝜔 B 𝜔 suc A = suc B) → ¬ (B A A B))
5 sucidg 4098 . . . . . . . . . . . 12 (B 𝜔 → B suc B)
6 eleq2 2079 . . . . . . . . . . . 12 (suc A = suc B → (B suc AB suc B))
75, 6syl5ibrcom 146 . . . . . . . . . . 11 (B 𝜔 → (suc A = suc BB suc A))
8 elsucg 4086 . . . . . . . . . . 11 (B 𝜔 → (B suc A ↔ (B A B = A)))
97, 8sylibd 138 . . . . . . . . . 10 (B 𝜔 → (suc A = suc B → (B A B = A)))
109imp 115 . . . . . . . . 9 ((B 𝜔 suc A = suc B) → (B A B = A))
11103adant1 908 . . . . . . . 8 ((A 𝜔 B 𝜔 suc A = suc B) → (B A B = A))
12 sucidg 4098 . . . . . . . . . . . 12 (A 𝜔 → A suc A)
13 eleq2 2079 . . . . . . . . . . . 12 (suc A = suc B → (A suc AA suc B))
1412, 13syl5ibcom 144 . . . . . . . . . . 11 (A 𝜔 → (suc A = suc BA suc B))
15 elsucg 4086 . . . . . . . . . . 11 (A 𝜔 → (A suc B ↔ (A B A = B)))
1614, 15sylibd 138 . . . . . . . . . 10 (A 𝜔 → (suc A = suc B → (A B A = B)))
1716imp 115 . . . . . . . . 9 ((A 𝜔 suc A = suc B) → (A B A = B))
18173adant2 909 . . . . . . . 8 ((A 𝜔 B 𝜔 suc A = suc B) → (A B A = B))
1911, 18jca 290 . . . . . . 7 ((A 𝜔 B 𝜔 suc A = suc B) → ((B A B = A) (A B A = B)))
20 eqcom 2020 . . . . . . . . 9 (B = AA = B)
2120orbi2i 666 . . . . . . . 8 ((B A B = A) ↔ (B A A = B))
2221anbi1i 434 . . . . . . 7 (((B A B = A) (A B A = B)) ↔ ((B A A = B) (A B A = B)))
2319, 22sylib 127 . . . . . 6 ((A 𝜔 B 𝜔 suc A = suc B) → ((B A A = B) (A B A = B)))
24 ordir 718 . . . . . 6 (((B A A B) A = B) ↔ ((B A A = B) (A B A = B)))
2523, 24sylibr 137 . . . . 5 ((A 𝜔 B 𝜔 suc A = suc B) → ((B A A B) A = B))
2625ord 630 . . . 4 ((A 𝜔 B 𝜔 suc A = suc B) → (¬ (B A A B) → A = B))
274, 26mpd 13 . . 3 ((A 𝜔 B 𝜔 suc A = suc B) → A = B)
28273expia 1090 . 2 ((A 𝜔 B 𝜔) → (suc A = suc BA = B))
29 suceq 4084 . 2 (A = B → suc A = suc B)
3028, 29impbid1 130 1 ((A 𝜔 B 𝜔) → (suc A = suc BA = B))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616   ∧ w3a 871   = wceq 1226   ∈ wcel 1370  suc csuc 4047  𝜔com 4236 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-nul 3853  ax-pr 3914  ax-un 4116  ax-bd0 7179  ax-bdor 7182  ax-bdn 7183  ax-bdal 7184  ax-bdex 7185  ax-bdeq 7186  ax-bdel 7187  ax-bdsb 7188  ax-bdsep 7250  ax-infvn 7302 This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-rab 2289  df-v 2533  df-dif 2893  df-un 2895  df-in 2897  df-ss 2904  df-nul 3198  df-sn 3352  df-pr 3353  df-uni 3551  df-int 3586  df-suc 4053  df-iom 4237  df-bdc 7207  df-bj-ind 7289 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator