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

Theorem ordtri3or 6418
Description: A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38. Theorem 1.9(iii) of [Schloeder] p. 1. (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 6416 . . . . . 6 ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴𝐵))
2 ordirr 6404 . . . . . 6 (Ord (𝐴𝐵) → ¬ (𝐴𝐵) ∈ (𝐴𝐵))
31, 2syl 17 . . . . 5 ((Ord 𝐴 ∧ Ord 𝐵) → ¬ (𝐴𝐵) ∈ (𝐴𝐵))
4 ianor 983 . . . . . 6 (¬ ((𝐴𝐵) ∈ 𝐴 ∧ (𝐵𝐴) ∈ 𝐵) ↔ (¬ (𝐴𝐵) ∈ 𝐴 ∨ ¬ (𝐵𝐴) ∈ 𝐵))
5 elin 3979 . . . . . . 7 ((𝐴𝐵) ∈ (𝐴𝐵) ↔ ((𝐴𝐵) ∈ 𝐴 ∧ (𝐴𝐵) ∈ 𝐵))
6 incom 4217 . . . . . . . . 9 (𝐴𝐵) = (𝐵𝐴)
76eleq1i 2830 . . . . . . . 8 ((𝐴𝐵) ∈ 𝐵 ↔ (𝐵𝐴) ∈ 𝐵)
87anbi2i 623 . . . . . . 7 (((𝐴𝐵) ∈ 𝐴 ∧ (𝐴𝐵) ∈ 𝐵) ↔ ((𝐴𝐵) ∈ 𝐴 ∧ (𝐵𝐴) ∈ 𝐵))
95, 8bitri 275 . . . . . 6 ((𝐴𝐵) ∈ (𝐴𝐵) ↔ ((𝐴𝐵) ∈ 𝐴 ∧ (𝐵𝐴) ∈ 𝐵))
104, 9xchnxbir 333 . . . . 5 (¬ (𝐴𝐵) ∈ (𝐴𝐵) ↔ (¬ (𝐴𝐵) ∈ 𝐴 ∨ ¬ (𝐵𝐴) ∈ 𝐵))
113, 10sylib 218 . . . 4 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴𝐵) ∈ 𝐴 ∨ ¬ (𝐵𝐴) ∈ 𝐵))
12 inss1 4245 . . . . . . . . . 10 (𝐴𝐵) ⊆ 𝐴
13 ordsseleq 6415 . . . . . . . . . 10 ((Ord (𝐴𝐵) ∧ Ord 𝐴) → ((𝐴𝐵) ⊆ 𝐴 ↔ ((𝐴𝐵) ∈ 𝐴 ∨ (𝐴𝐵) = 𝐴)))
1412, 13mpbii 233 . . . . . . . . 9 ((Ord (𝐴𝐵) ∧ Ord 𝐴) → ((𝐴𝐵) ∈ 𝐴 ∨ (𝐴𝐵) = 𝐴))
151, 14sylan 580 . . . . . . . 8 (((Ord 𝐴 ∧ Ord 𝐵) ∧ Ord 𝐴) → ((𝐴𝐵) ∈ 𝐴 ∨ (𝐴𝐵) = 𝐴))
1615anabss1 666 . . . . . . 7 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴𝐵) ∈ 𝐴 ∨ (𝐴𝐵) = 𝐴))
1716ord 864 . . . . . 6 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴𝐵) ∈ 𝐴 → (𝐴𝐵) = 𝐴))
18 dfss2 3981 . . . . . 6 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
1917, 18imbitrrdi 252 . . . . 5 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴𝐵) ∈ 𝐴𝐴𝐵))
20 ordin 6416 . . . . . . . . 9 ((Ord 𝐵 ∧ Ord 𝐴) → Ord (𝐵𝐴))
21 inss1 4245 . . . . . . . . . 10 (𝐵𝐴) ⊆ 𝐵
22 ordsseleq 6415 . . . . . . . . . 10 ((Ord (𝐵𝐴) ∧ Ord 𝐵) → ((𝐵𝐴) ⊆ 𝐵 ↔ ((𝐵𝐴) ∈ 𝐵 ∨ (𝐵𝐴) = 𝐵)))
2321, 22mpbii 233 . . . . . . . . 9 ((Ord (𝐵𝐴) ∧ Ord 𝐵) → ((𝐵𝐴) ∈ 𝐵 ∨ (𝐵𝐴) = 𝐵))
2420, 23sylan 580 . . . . . . . 8 (((Ord 𝐵 ∧ Ord 𝐴) ∧ Ord 𝐵) → ((𝐵𝐴) ∈ 𝐵 ∨ (𝐵𝐴) = 𝐵))
2524anabss4 667 . . . . . . 7 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐵𝐴) ∈ 𝐵 ∨ (𝐵𝐴) = 𝐵))
2625ord 864 . . . . . 6 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐵𝐴) ∈ 𝐵 → (𝐵𝐴) = 𝐵))
27 dfss2 3981 . . . . . 6 (𝐵𝐴 ↔ (𝐵𝐴) = 𝐵)
2826, 27imbitrrdi 252 . . . . 5 ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐵𝐴) ∈ 𝐵𝐵𝐴))
2919, 28orim12d 966 . . . 4 ((Ord 𝐴 ∧ Ord 𝐵) → ((¬ (𝐴𝐵) ∈ 𝐴 ∨ ¬ (𝐵𝐴) ∈ 𝐵) → (𝐴𝐵𝐵𝐴)))
3011, 29mpd 15 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵𝐵𝐴))
31 sspsstri 4115 . . 3 ((𝐴𝐵𝐵𝐴) ↔ (𝐴𝐵𝐴 = 𝐵𝐵𝐴))
3230, 31sylib 218 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))
33 ordelpss 6414 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵𝐴𝐵))
34 biidd 262 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵𝐴 = 𝐵))
35 ordelpss 6414 . . . 4 ((Ord 𝐵 ∧ Ord 𝐴) → (𝐵𝐴𝐵𝐴))
3635ancoms 458 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐵𝐴𝐵𝐴))
3733, 34, 363orbi123d 1434 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴𝐵𝐴 = 𝐵𝐵𝐴) ↔ (𝐴𝐵𝐴 = 𝐵𝐵𝐴)))
3832, 37mpbird 257 1 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3o 1085   = wceq 1537  wcel 2106  cin 3962  wss 3963  wpss 3964  Ord word 6385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389
This theorem is referenced by:  ordtri1  6419  epweon  7794  epweonALT  7795  ordeleqon  7801  poseq  8182  soseq  8183  smo11  8403  smoord  8404  omopth2  8621  ttrcltr  9754  r111  9813  tcrank  9922  domtriomlem  10480  axdc3lem2  10489  zorn2lem6  10539  grur1  10858  nosepon  27725  addsproplem7  28023  negsproplem7  28081  mulsproplem13  28169  mulsproplem14  28170  oneltri  43247
  Copyright terms: Public domain W3C validator