ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nntri3or GIF version

Theorem nntri3or 6185
Description: Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.)
Assertion
Ref Expression
nntri3or ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))

Proof of Theorem nntri3or
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2146 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
2 eqeq2 2092 . . . . 5 (𝑥 = 𝐵 → (𝐴 = 𝑥𝐴 = 𝐵))
3 eleq1 2145 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
41, 2, 33orbi123d 1243 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 = 𝑥𝑥𝐴) ↔ (𝐴𝐵𝐴 = 𝐵𝐵𝐴)))
54imbi2d 228 . . 3 (𝑥 = 𝐵 → ((𝐴 ∈ ω → (𝐴𝑥𝐴 = 𝑥𝑥𝐴)) ↔ (𝐴 ∈ ω → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))))
6 eleq2 2146 . . . . 5 (𝑥 = ∅ → (𝐴𝑥𝐴 ∈ ∅))
7 eqeq2 2092 . . . . 5 (𝑥 = ∅ → (𝐴 = 𝑥𝐴 = ∅))
8 eleq1 2145 . . . . 5 (𝑥 = ∅ → (𝑥𝐴 ↔ ∅ ∈ 𝐴))
96, 7, 83orbi123d 1243 . . . 4 (𝑥 = ∅ → ((𝐴𝑥𝐴 = 𝑥𝑥𝐴) ↔ (𝐴 ∈ ∅ ∨ 𝐴 = ∅ ∨ ∅ ∈ 𝐴)))
10 eleq2 2146 . . . . 5 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
11 eqeq2 2092 . . . . 5 (𝑥 = 𝑦 → (𝐴 = 𝑥𝐴 = 𝑦))
12 eleq1 2145 . . . . 5 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
1310, 11, 123orbi123d 1243 . . . 4 (𝑥 = 𝑦 → ((𝐴𝑥𝐴 = 𝑥𝑥𝐴) ↔ (𝐴𝑦𝐴 = 𝑦𝑦𝐴)))
14 eleq2 2146 . . . . 5 (𝑥 = suc 𝑦 → (𝐴𝑥𝐴 ∈ suc 𝑦))
15 eqeq2 2092 . . . . 5 (𝑥 = suc 𝑦 → (𝐴 = 𝑥𝐴 = suc 𝑦))
16 eleq1 2145 . . . . 5 (𝑥 = suc 𝑦 → (𝑥𝐴 ↔ suc 𝑦𝐴))
1714, 15, 163orbi123d 1243 . . . 4 (𝑥 = suc 𝑦 → ((𝐴𝑥𝐴 = 𝑥𝑥𝐴) ↔ (𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴)))
18 0elnn 4394 . . . . 5 (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∅ ∈ 𝐴))
19 olc 665 . . . . . 6 ((𝐴 = ∅ ∨ ∅ ∈ 𝐴) → (𝐴 ∈ ∅ ∨ (𝐴 = ∅ ∨ ∅ ∈ 𝐴)))
20 3orass 923 . . . . . 6 ((𝐴 ∈ ∅ ∨ 𝐴 = ∅ ∨ ∅ ∈ 𝐴) ↔ (𝐴 ∈ ∅ ∨ (𝐴 = ∅ ∨ ∅ ∈ 𝐴)))
2119, 20sylibr 132 . . . . 5 ((𝐴 = ∅ ∨ ∅ ∈ 𝐴) → (𝐴 ∈ ∅ ∨ 𝐴 = ∅ ∨ ∅ ∈ 𝐴))
2218, 21syl 14 . . . 4 (𝐴 ∈ ω → (𝐴 ∈ ∅ ∨ 𝐴 = ∅ ∨ ∅ ∈ 𝐴))
23 df-3or 921 . . . . . 6 ((𝐴𝑦𝐴 = 𝑦𝑦𝐴) ↔ ((𝐴𝑦𝐴 = 𝑦) ∨ 𝑦𝐴))
24 elex 2621 . . . . . . . 8 (𝑦 ∈ ω → 𝑦 ∈ V)
25 elsuc2g 4195 . . . . . . . . 9 (𝑦 ∈ V → (𝐴 ∈ suc 𝑦 ↔ (𝐴𝑦𝐴 = 𝑦)))
26 3mix1 1108 . . . . . . . . 9 (𝐴 ∈ suc 𝑦 → (𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴))
2725, 26syl6bir 162 . . . . . . . 8 (𝑦 ∈ V → ((𝐴𝑦𝐴 = 𝑦) → (𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴)))
2824, 27syl 14 . . . . . . 7 (𝑦 ∈ ω → ((𝐴𝑦𝐴 = 𝑦) → (𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴)))
29 nnsucelsuc 6183 . . . . . . . . 9 (𝐴 ∈ ω → (𝑦𝐴 ↔ suc 𝑦 ∈ suc 𝐴))
30 elsuci 4193 . . . . . . . . 9 (suc 𝑦 ∈ suc 𝐴 → (suc 𝑦𝐴 ∨ suc 𝑦 = 𝐴))
3129, 30syl6bi 161 . . . . . . . 8 (𝐴 ∈ ω → (𝑦𝐴 → (suc 𝑦𝐴 ∨ suc 𝑦 = 𝐴)))
32 eqcom 2085 . . . . . . . . . . . . 13 (suc 𝑦 = 𝐴𝐴 = suc 𝑦)
3332orbi2i 712 . . . . . . . . . . . 12 ((suc 𝑦𝐴 ∨ suc 𝑦 = 𝐴) ↔ (suc 𝑦𝐴𝐴 = suc 𝑦))
3433biimpi 118 . . . . . . . . . . 11 ((suc 𝑦𝐴 ∨ suc 𝑦 = 𝐴) → (suc 𝑦𝐴𝐴 = suc 𝑦))
3534orcomd 681 . . . . . . . . . 10 ((suc 𝑦𝐴 ∨ suc 𝑦 = 𝐴) → (𝐴 = suc 𝑦 ∨ suc 𝑦𝐴))
3635olcd 686 . . . . . . . . 9 ((suc 𝑦𝐴 ∨ suc 𝑦 = 𝐴) → (𝐴 ∈ suc 𝑦 ∨ (𝐴 = suc 𝑦 ∨ suc 𝑦𝐴)))
37 3orass 923 . . . . . . . . 9 ((𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴) ↔ (𝐴 ∈ suc 𝑦 ∨ (𝐴 = suc 𝑦 ∨ suc 𝑦𝐴)))
3836, 37sylibr 132 . . . . . . . 8 ((suc 𝑦𝐴 ∨ suc 𝑦 = 𝐴) → (𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴))
3931, 38syl6 33 . . . . . . 7 (𝐴 ∈ ω → (𝑦𝐴 → (𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴)))
4028, 39jaao 672 . . . . . 6 ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (((𝐴𝑦𝐴 = 𝑦) ∨ 𝑦𝐴) → (𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴)))
4123, 40syl5bi 150 . . . . 5 ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → ((𝐴𝑦𝐴 = 𝑦𝑦𝐴) → (𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴)))
4241ex 113 . . . 4 (𝑦 ∈ ω → (𝐴 ∈ ω → ((𝐴𝑦𝐴 = 𝑦𝑦𝐴) → (𝐴 ∈ suc 𝑦𝐴 = suc 𝑦 ∨ suc 𝑦𝐴))))
439, 13, 17, 22, 42finds2 4378 . . 3 (𝑥 ∈ ω → (𝐴 ∈ ω → (𝐴𝑥𝐴 = 𝑥𝑥𝐴)))
445, 43vtoclga 2675 . 2 (𝐵 ∈ ω → (𝐴 ∈ ω → (𝐴𝐵𝐴 = 𝐵𝐵𝐴)))
4544impcom 123 1 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wo 662  w3o 919   = wceq 1285  wcel 1434  Vcvv 2612  c0 3269  suc csuc 4155  ωcom 4367
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 3999  ax-un 4223  ax-iinf 4365
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-uni 3628  df-int 3663  df-tr 3902  df-iord 4156  df-on 4158  df-suc 4161  df-iom 4368
This theorem is referenced by:  nntri2  6186  nntri1  6188  nntri3  6189  nntri2or2  6190  nndceq  6191  nndcel  6192  nnsseleq  6193  nnawordex  6216  nnwetri  6552  ltsopi  6781  pitri3or  6783  frec2uzlt2d  9699
  Copyright terms: Public domain W3C validator