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

Theorem ordtri1 5475
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  A  /\  Ord  B )  ->  ( A  C_  B  <->  -.  B  e.  A ) )

Proof of Theorem ordtri1
StepHypRef Expression
1 ordsseleq 5471 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  C_  B  <->  ( A  e.  B  \/  A  =  B ) ) )
2 ordn2lp 5462 . . . . 5  |-  ( Ord 
A  ->  -.  ( A  e.  B  /\  B  e.  A )
)
3 imnan 428 . . . . 5  |-  ( ( A  e.  B  ->  -.  B  e.  A
)  <->  -.  ( A  e.  B  /\  B  e.  A ) )
42, 3sylibr 217 . . . 4  |-  ( Ord 
A  ->  ( A  e.  B  ->  -.  B  e.  A ) )
5 ordirr 5460 . . . . 5  |-  ( Ord 
B  ->  -.  B  e.  B )
6 eleq2 2529 . . . . . 6  |-  ( A  =  B  ->  ( B  e.  A  <->  B  e.  B ) )
76notbid 300 . . . . 5  |-  ( A  =  B  ->  ( -.  B  e.  A  <->  -.  B  e.  B ) )
85, 7syl5ibrcom 230 . . . 4  |-  ( Ord 
B  ->  ( A  =  B  ->  -.  B  e.  A ) )
94, 8jaao 516 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( A  e.  B  \/  A  =  B )  ->  -.  B  e.  A
) )
10 ordtri3or 5474 . . . . . 6  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A ) )
11 df-3or 992 . . . . . 6  |-  ( ( A  e.  B  \/  A  =  B  \/  B  e.  A )  <->  ( ( A  e.  B  \/  A  =  B
)  \/  B  e.  A ) )
1210, 11sylib 201 . . . . 5  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( A  e.  B  \/  A  =  B )  \/  B  e.  A
) )
1312orcomd 394 . . . 4  |-  ( ( Ord  A  /\  Ord  B )  ->  ( B  e.  A  \/  ( A  e.  B  \/  A  =  B )
) )
1413ord 383 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( -.  B  e.  A  ->  ( A  e.  B  \/  A  =  B )
) )
159, 14impbid 195 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( A  e.  B  \/  A  =  B )  <->  -.  B  e.  A ) )
161, 15bitrd 261 1  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  C_  B  <->  -.  B  e.  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    \/ w3o 990    = wceq 1455    e. wcel 1898    C_ wss 3416   Ord word 5441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-tr 4512  df-eprel 4764  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-ord 5445
This theorem is referenced by:  ontri1  5476  ordtri2  5477  ordtri4  5479  ordtr3  5487  ordintdif  5491  ordtri2or  5537  ordsucss  6672  ordsucsssuc  6677  ordsucuniel  6678  limsssuc  6704  ssnlim  6737  smoword  7111  tfrlem15  7136  nnaword  7354  nnawordex  7364  onomeneq  7788  nndomo  7792  isfinite2  7855  unfilem1  7861  wofib  8086  cantnflem1  8220  alephgeom  8539  alephdom2  8544  cflim2  8719  fin67  8851  winainflem  9144  finminlem  31023
  Copyright terms: Public domain W3C validator