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

Theorem ordtri3or 5968
Description: A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38. (Contributed by NM, 10-May-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
ordtri3or ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))

Proof of Theorem ordtri3or
StepHypRef Expression
1 ordin 5966 . . . . . 6 ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴𝐵))
2 ordirr 5954 . . . . . 6 (Ord (𝐴𝐵) → ¬ (𝐴𝐵) ∈ (𝐴𝐵))
31, 2syl 17 . . . . 5 ((Ord 𝐴 ∧ Ord 𝐵) → ¬ (𝐴𝐵) ∈ (𝐴𝐵))
4 ianor 995 . . . . . 6 (¬ ((𝐴𝐵) ∈ 𝐴 ∧ (𝐵𝐴) ∈ 𝐵) ↔ (¬ (𝐴𝐵) ∈ 𝐴 ∨ ¬ (𝐵𝐴) ∈ 𝐵))
5 elin 3995 . . . . . . 7 ((𝐴𝐵) ∈ (𝐴𝐵) ↔ ((𝐴𝐵) ∈ 𝐴 ∧ (𝐴𝐵) ∈ 𝐵))
6 incom 4004 . . . . . . . . 9 (𝐴𝐵) = (𝐵𝐴)
76eleq1i 2876 . . . . . . . 8 ((𝐴𝐵) ∈ 𝐵 ↔ (𝐵𝐴) ∈ 𝐵)
87anbi2i 611 . . . . . . 7 (((𝐴𝐵) ∈ 𝐴 ∧ (𝐴𝐵) ∈ 𝐵) ↔ ((𝐴𝐵) ∈ 𝐴 ∧ (𝐵𝐴) ∈ 𝐵))
95, 8bitri 266 . . . . . 6 ((𝐴𝐵) ∈ (𝐴𝐵) ↔ ((𝐴𝐵) ∈ 𝐴 ∧ (𝐵𝐴) ∈ 𝐵))
104, 9xchnxbir 324 . . . . 5 (¬ (𝐴𝐵) ∈ (𝐴𝐵) ↔ (¬ (𝐴𝐵) ∈ 𝐴 ∨ ¬ (𝐵𝐴) ∈ 𝐵))
113, 10sylib 209 . . . 4 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴𝐵) ∈ 𝐴 ∨ ¬ (𝐵𝐴) ∈ 𝐵))
12 inss1 4029 . . . . . . . . . 10 (𝐴𝐵) ⊆ 𝐴
13 ordsseleq 5965 . . . . . . . . . 10 ((Ord (𝐴𝐵) ∧ Ord 𝐴) → ((𝐴𝐵) ⊆ 𝐴 ↔ ((𝐴𝐵) ∈ 𝐴 ∨ (𝐴𝐵) = 𝐴)))
1412, 13mpbii 224 . . . . . . . . 9 ((Ord (𝐴𝐵) ∧ Ord 𝐴) → ((𝐴𝐵) ∈ 𝐴 ∨ (𝐴𝐵) = 𝐴))
151, 14sylan 571 . . . . . . . 8 (((Ord 𝐴 ∧ Ord 𝐵) ∧ Ord 𝐴) → ((𝐴𝐵) ∈ 𝐴 ∨ (𝐴𝐵) = 𝐴))
1615anabss1 648 . . . . . . 7 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴𝐵) ∈ 𝐴 ∨ (𝐴𝐵) = 𝐴))
1716ord 882 . . . . . 6 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴𝐵) ∈ 𝐴 → (𝐴𝐵) = 𝐴))
18 df-ss 3783 . . . . . 6 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
1917, 18syl6ibr 243 . . . . 5 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴𝐵) ∈ 𝐴𝐴𝐵))
20 ordin 5966 . . . . . . . . 9 ((Ord 𝐵 ∧ Ord 𝐴) → Ord (𝐵𝐴))
21 inss1 4029 . . . . . . . . . 10 (𝐵𝐴) ⊆ 𝐵
22 ordsseleq 5965 . . . . . . . . . 10 ((Ord (𝐵𝐴) ∧ Ord 𝐵) → ((𝐵𝐴) ⊆ 𝐵 ↔ ((𝐵𝐴) ∈ 𝐵 ∨ (𝐵𝐴) = 𝐵)))
2321, 22mpbii 224 . . . . . . . . 9 ((Ord (𝐵𝐴) ∧ Ord 𝐵) → ((𝐵𝐴) ∈ 𝐵 ∨ (𝐵𝐴) = 𝐵))
2420, 23sylan 571 . . . . . . . 8 (((Ord 𝐵 ∧ Ord 𝐴) ∧ Ord 𝐵) → ((𝐵𝐴) ∈ 𝐵 ∨ (𝐵𝐴) = 𝐵))
2524anabss4 649 . . . . . . 7 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐵𝐴) ∈ 𝐵 ∨ (𝐵𝐴) = 𝐵))
2625ord 882 . . . . . 6 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐵𝐴) ∈ 𝐵 → (𝐵𝐴) = 𝐵))
27 df-ss 3783 . . . . . 6 (𝐵𝐴 ↔ (𝐵𝐴) = 𝐵)
2826, 27syl6ibr 243 . . . . 5 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐵𝐴) ∈ 𝐵𝐵𝐴))
2919, 28orim12d 978 . . . 4 ((Ord 𝐴 ∧ Ord 𝐵) → ((¬ (𝐴𝐵) ∈ 𝐴 ∨ ¬ (𝐵𝐴) ∈ 𝐵) → (𝐴𝐵𝐵𝐴)))
3011, 29mpd 15 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵𝐵𝐴))
31 sspsstri 3907 . . 3 ((𝐴𝐵𝐵𝐴) ↔ (𝐴𝐵𝐴 = 𝐵𝐵𝐴))
3230, 31sylib 209 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))
33 ordelpss 5964 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵𝐴𝐵))
34 biidd 253 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵𝐴 = 𝐵))
35 ordelpss 5964 . . . 4 ((Ord 𝐵 ∧ Ord 𝐴) → (𝐵𝐴𝐵𝐴))
3635ancoms 448 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐵𝐴𝐵𝐴))
3733, 34, 363orbi123d 1552 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴𝐵𝐴 = 𝐵𝐵𝐴) ↔ (𝐴𝐵𝐴 = 𝐵𝐵𝐴)))
3832, 37mpbird 248 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  cin 3768  wss 3769  wpss 3770  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:  ordtri1  5969  ordon  7208  ordeleqon  7214  smo11  7693  smoord  7694  omopth2  7897  r111  8881  tcrank  8990  domtriomlem  9545  axdc3lem2  9554  zorn2lem6  9604  grur1  9923  poseq  32072  soseq  32073  nosepon  32137
  Copyright terms: Public domain W3C validator