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

Theorem ordtri3or 4772
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  A  /\  Ord  B )  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A ) )

Proof of Theorem ordtri3or
StepHypRef Expression
1 ordin 4770 . . . . . 6  |-  ( ( Ord  A  /\  Ord  B )  ->  Ord  ( A  i^i  B ) )
2 ordirr 4758 . . . . . 6  |-  ( Ord  ( A  i^i  B
)  ->  -.  ( A  i^i  B )  e.  ( A  i^i  B
) )
31, 2syl 16 . . . . 5  |-  ( ( Ord  A  /\  Ord  B )  ->  -.  ( A  i^i  B )  e.  ( A  i^i  B
) )
4 ianor 488 . . . . . 6  |-  ( -.  ( ( A  i^i  B )  e.  A  /\  ( B  i^i  A )  e.  B )  <->  ( -.  ( A  i^i  B )  e.  A  \/  -.  ( B  i^i  A )  e.  B ) )
5 elin 3560 . . . . . . 7  |-  ( ( A  i^i  B )  e.  ( A  i^i  B )  <->  ( ( A  i^i  B )  e.  A  /\  ( A  i^i  B )  e.  B ) )
6 incom 3564 . . . . . . . . 9  |-  ( A  i^i  B )  =  ( B  i^i  A
)
76eleq1i 2506 . . . . . . . 8  |-  ( ( A  i^i  B )  e.  B  <->  ( B  i^i  A )  e.  B
)
87anbi2i 694 . . . . . . 7  |-  ( ( ( A  i^i  B
)  e.  A  /\  ( A  i^i  B )  e.  B )  <->  ( ( A  i^i  B )  e.  A  /\  ( B  i^i  A )  e.  B ) )
95, 8bitri 249 . . . . . 6  |-  ( ( A  i^i  B )  e.  ( A  i^i  B )  <->  ( ( A  i^i  B )  e.  A  /\  ( B  i^i  A )  e.  B ) )
104, 9xchnxbir 309 . . . . 5  |-  ( -.  ( A  i^i  B
)  e.  ( A  i^i  B )  <->  ( -.  ( A  i^i  B )  e.  A  \/  -.  ( B  i^i  A )  e.  B ) )
113, 10sylib 196 . . . 4  |-  ( ( Ord  A  /\  Ord  B )  ->  ( -.  ( A  i^i  B )  e.  A  \/  -.  ( B  i^i  A )  e.  B ) )
12 inss1 3591 . . . . . . . . . 10  |-  ( A  i^i  B )  C_  A
13 ordsseleq 4769 . . . . . . . . . 10  |-  ( ( Ord  ( A  i^i  B )  /\  Ord  A
)  ->  ( ( A  i^i  B )  C_  A 
<->  ( ( A  i^i  B )  e.  A  \/  ( A  i^i  B )  =  A ) ) )
1412, 13mpbii 211 . . . . . . . . 9  |-  ( ( Ord  ( A  i^i  B )  /\  Ord  A
)  ->  ( ( A  i^i  B )  e.  A  \/  ( A  i^i  B )  =  A ) )
151, 14sylan 471 . . . . . . . 8  |-  ( ( ( Ord  A  /\  Ord  B )  /\  Ord  A )  ->  ( ( A  i^i  B )  e.  A  \/  ( A  i^i  B )  =  A ) )
1615anabss1 810 . . . . . . 7  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( A  i^i  B )  e.  A  \/  ( A  i^i  B )  =  A ) )
1716ord 377 . . . . . 6  |-  ( ( Ord  A  /\  Ord  B )  ->  ( -.  ( A  i^i  B )  e.  A  ->  ( A  i^i  B )  =  A ) )
18 df-ss 3363 . . . . . 6  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
1917, 18syl6ibr 227 . . . . 5  |-  ( ( Ord  A  /\  Ord  B )  ->  ( -.  ( A  i^i  B )  e.  A  ->  A  C_  B ) )
20 ordin 4770 . . . . . . . . 9  |-  ( ( Ord  B  /\  Ord  A )  ->  Ord  ( B  i^i  A ) )
21 inss1 3591 . . . . . . . . . 10  |-  ( B  i^i  A )  C_  B
22 ordsseleq 4769 . . . . . . . . . 10  |-  ( ( Ord  ( B  i^i  A )  /\  Ord  B
)  ->  ( ( B  i^i  A )  C_  B 
<->  ( ( B  i^i  A )  e.  B  \/  ( B  i^i  A )  =  B ) ) )
2321, 22mpbii 211 . . . . . . . . 9  |-  ( ( Ord  ( B  i^i  A )  /\  Ord  B
)  ->  ( ( B  i^i  A )  e.  B  \/  ( B  i^i  A )  =  B ) )
2420, 23sylan 471 . . . . . . . 8  |-  ( ( ( Ord  B  /\  Ord  A )  /\  Ord  B )  ->  ( ( B  i^i  A )  e.  B  \/  ( B  i^i  A )  =  B ) )
2524anabss4 811 . . . . . . 7  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( B  i^i  A )  e.  B  \/  ( B  i^i  A )  =  B ) )
2625ord 377 . . . . . 6  |-  ( ( Ord  A  /\  Ord  B )  ->  ( -.  ( B  i^i  A )  e.  B  ->  ( B  i^i  A )  =  B ) )
27 df-ss 3363 . . . . . 6  |-  ( B 
C_  A  <->  ( B  i^i  A )  =  B )
2826, 27syl6ibr 227 . . . . 5  |-  ( ( Ord  A  /\  Ord  B )  ->  ( -.  ( B  i^i  A )  e.  B  ->  B  C_  A ) )
2919, 28orim12d 834 . . . 4  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( -.  ( A  i^i  B
)  e.  A  \/  -.  ( B  i^i  A
)  e.  B )  ->  ( A  C_  B  \/  B  C_  A
) ) )
3011, 29mpd 15 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  C_  B  \/  B  C_  A ) )
31 sspsstri 3479 . . 3  |-  ( ( A  C_  B  \/  B  C_  A )  <->  ( A  C.  B  \/  A  =  B  \/  B  C.  A ) )
3230, 31sylib 196 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  C.  B  \/  A  =  B  \/  B  C.  A ) )
33 ordelpss 4768 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  e.  B  <->  A  C.  B ) )
34 biidd 237 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  =  B  <->  A  =  B
) )
35 ordelpss 4768 . . . 4  |-  ( ( Ord  B  /\  Ord  A )  ->  ( B  e.  A  <->  B  C.  A ) )
3635ancoms 453 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( B  e.  A  <->  B  C.  A ) )
3733, 34, 363orbi123d 1288 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( A  e.  B  \/  A  =  B  \/  B  e.  A )  <->  ( A  C.  B  \/  A  =  B  \/  B  C.  A ) ) )
3832, 37mpbird 232 1  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    \/ w3o 964    = wceq 1369    e. wcel 1756    i^i cin 3348    C_ wss 3349    C. wpss 3350   Ord word 4739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-tr 4407  df-eprel 4653  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743
This theorem is referenced by:  ordtri1  4773  ordtri3  4776  ordon  6415  ordeleqon  6421  smo11  6846  smoord  6847  omopth2  7044  r111  8003  tcrank  8112  domtriomlem  8632  axdc3lem2  8641  zorn2lem6  8691  grur1  9008  poseq  27736  soseq  27737
  Copyright terms: Public domain W3C validator