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

Theorem ordtri3 5478
Description: A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
ordtri3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  =  B  <->  -.  ( A  e.  B  \/  B  e.  A ) ) )

Proof of Theorem ordtri3
StepHypRef Expression
1 ordirr 5460 . . . . . 6  |-  ( Ord 
A  ->  -.  A  e.  A )
2 eleq2 2496 . . . . . . 7  |-  ( A  =  B  ->  ( A  e.  A  <->  A  e.  B ) )
32notbid 295 . . . . . 6  |-  ( A  =  B  ->  ( -.  A  e.  A  <->  -.  A  e.  B ) )
41, 3syl5ib 222 . . . . 5  |-  ( A  =  B  ->  ( Ord  A  ->  -.  A  e.  B ) )
5 ordirr 5460 . . . . . 6  |-  ( Ord 
B  ->  -.  B  e.  B )
6 eleq2 2496 . . . . . . 7  |-  ( A  =  B  ->  ( B  e.  A  <->  B  e.  B ) )
76notbid 295 . . . . . 6  |-  ( A  =  B  ->  ( -.  B  e.  A  <->  -.  B  e.  B ) )
85, 7syl5ibr 224 . . . . 5  |-  ( A  =  B  ->  ( Ord  B  ->  -.  B  e.  A ) )
94, 8anim12d 565 . . . 4  |-  ( A  =  B  ->  (
( Ord  A  /\  Ord  B )  ->  ( -.  A  e.  B  /\  -.  B  e.  A
) ) )
109com12 32 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  =  B  ->  ( -.  A  e.  B  /\  -.  B  e.  A
) ) )
11 pm4.56 497 . . 3  |-  ( ( -.  A  e.  B  /\  -.  B  e.  A
)  <->  -.  ( A  e.  B  \/  B  e.  A ) )
1210, 11syl6ib 229 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  =  B  ->  -.  ( A  e.  B  \/  B  e.  A )
) )
13 ordtri3or 5474 . . . . 5  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A ) )
14 df-3or 983 . . . . 5  |-  ( ( A  e.  B  \/  A  =  B  \/  B  e.  A )  <->  ( ( A  e.  B  \/  A  =  B
)  \/  B  e.  A ) )
1513, 14sylib 199 . . . 4  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( A  e.  B  \/  A  =  B )  \/  B  e.  A
) )
16 or32 529 . . . 4  |-  ( ( ( A  e.  B  \/  A  =  B
)  \/  B  e.  A )  <->  ( ( A  e.  B  \/  B  e.  A )  \/  A  =  B
) )
1715, 16sylib 199 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( A  e.  B  \/  B  e.  A )  \/  A  =  B
) )
1817ord 378 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( -.  ( A  e.  B  \/  B  e.  A
)  ->  A  =  B ) )
1912, 18impbid 193 1  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  =  B  <->  -.  ( A  e.  B  \/  B  e.  A ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    \/ w3o 981    = wceq 1437    e. wcel 1872   Ord word 5441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-tr 4519  df-eprel 4764  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-ord 5445
This theorem is referenced by:  ordunisuc2  6685  tz7.48lem  7169  oacan  7260  omcan  7281  oecan  7301  omsmo  7366  omopthi  7369  inf3lem6  8147  cantnfp1lem3  8193  infpssrlem5  8744  fin23lem24  8759  isf32lem4  8793  om2uzf1oi  12173  nodenselem4  30578
  Copyright terms: Public domain W3C validator