MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtri1 Structured version   Visualization version   GIF version

Theorem ordtri1 5969
Description: A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
ordtri1 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵 ↔ ¬ 𝐵𝐴))

Proof of Theorem ordtri1
StepHypRef Expression
1 ordsseleq 5965 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))
2 ordn2lp 5956 . . . . 5 (Ord 𝐴 → ¬ (𝐴𝐵𝐵𝐴))
3 imnan 388 . . . . 5 ((𝐴𝐵 → ¬ 𝐵𝐴) ↔ ¬ (𝐴𝐵𝐵𝐴))
42, 3sylibr 225 . . . 4 (Ord 𝐴 → (𝐴𝐵 → ¬ 𝐵𝐴))
5 ordirr 5954 . . . . 5 (Ord 𝐵 → ¬ 𝐵𝐵)
6 eleq2 2874 . . . . . 6 (𝐴 = 𝐵 → (𝐵𝐴𝐵𝐵))
76notbid 309 . . . . 5 (𝐴 = 𝐵 → (¬ 𝐵𝐴 ↔ ¬ 𝐵𝐵))
85, 7syl5ibrcom 238 . . . 4 (Ord 𝐵 → (𝐴 = 𝐵 → ¬ 𝐵𝐴))
94, 8jaao 968 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴𝐵𝐴 = 𝐵) → ¬ 𝐵𝐴))
10 ordtri3or 5968 . . . . . 6 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))
11 df-3or 1101 . . . . . 6 ((𝐴𝐵𝐴 = 𝐵𝐵𝐴) ↔ ((𝐴𝐵𝐴 = 𝐵) ∨ 𝐵𝐴))
1210, 11sylib 209 . . . . 5 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴𝐵𝐴 = 𝐵) ∨ 𝐵𝐴))
1312orcomd 889 . . . 4 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐵𝐴 ∨ (𝐴𝐵𝐴 = 𝐵)))
1413ord 882 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ 𝐵𝐴 → (𝐴𝐵𝐴 = 𝐵)))
159, 14impbid 203 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴𝐵𝐴 = 𝐵) ↔ ¬ 𝐵𝐴))
161, 15bitrd 270 1 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3o 1099   = wceq 1637  wcel 2156  wss 3769  Ord word 5935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-tr 4947  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-ord 5939
This theorem is referenced by:  ontri1  5970  ordtri2  5971  ordtri4  5974  ordtr3  5982  ordtr3OLD  5983  ordintdif  5987  ordtri2or  6035  ordsucss  7248  ordsucsssuc  7253  ordsucuniel  7254  limsssuc  7280  ssnlim  7313  smoword  7699  tfrlem15  7724  nnaword  7944  nnawordex  7954  onomeneq  8389  nndomo  8393  isfinite2  8457  unfilem1  8463  wofib  8689  cantnflem1  8833  alephgeom  9188  alephdom2  9193  cflim2  9370  fin67  9502  winainflem  9800  finminlem  32633
  Copyright terms: Public domain W3C validator