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

Theorem ordtri3 4465
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 4447 . . . . . 6  |-  ( Ord 
A  ->  -.  A  e.  A )
2 eleq2 2377 . . . . . . 7  |-  ( A  =  B  ->  ( A  e.  A  <->  A  e.  B ) )
32notbid 285 . . . . . 6  |-  ( A  =  B  ->  ( -.  A  e.  A  <->  -.  A  e.  B ) )
41, 3syl5ib 210 . . . . 5  |-  ( A  =  B  ->  ( Ord  A  ->  -.  A  e.  B ) )
5 ordirr 4447 . . . . . 6  |-  ( Ord 
B  ->  -.  B  e.  B )
6 eleq2 2377 . . . . . . 7  |-  ( A  =  B  ->  ( B  e.  A  <->  B  e.  B ) )
76notbid 285 . . . . . 6  |-  ( A  =  B  ->  ( -.  B  e.  A  <->  -.  B  e.  B ) )
85, 7syl5ibr 212 . . . . 5  |-  ( A  =  B  ->  ( Ord  B  ->  -.  B  e.  A ) )
94, 8anim12d 546 . . . 4  |-  ( A  =  B  ->  (
( Ord  A  /\  Ord  B )  ->  ( -.  A  e.  B  /\  -.  B  e.  A
) ) )
109com12 27 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  =  B  ->  ( -.  A  e.  B  /\  -.  B  e.  A
) ) )
11 pm4.56 481 . . 3  |-  ( ( -.  A  e.  B  /\  -.  B  e.  A
)  <->  -.  ( A  e.  B  \/  B  e.  A ) )
1210, 11syl6ib 217 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  =  B  ->  -.  ( A  e.  B  \/  B  e.  A )
) )
13 ordtri3or 4461 . . . . 5  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A ) )
14 df-3or 935 . . . . 5  |-  ( ( A  e.  B  \/  A  =  B  \/  B  e.  A )  <->  ( ( A  e.  B  \/  A  =  B
)  \/  B  e.  A ) )
1513, 14sylib 188 . . . 4  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( A  e.  B  \/  A  =  B )  \/  B  e.  A
) )
16 or32 513 . . . 4  |-  ( ( ( A  e.  B  \/  A  =  B
)  \/  B  e.  A )  <->  ( ( A  e.  B  \/  B  e.  A )  \/  A  =  B
) )
1715, 16sylib 188 . . 3  |-  ( ( Ord  A  /\  Ord  B )  ->  ( ( A  e.  B  \/  B  e.  A )  \/  A  =  B
) )
1817ord 366 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( -.  ( A  e.  B  \/  B  e.  A
)  ->  A  =  B ) )
1912, 18impbid 183 1  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  =  B  <->  -.  ( A  e.  B  \/  B  e.  A ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    \/ w3o 933    = wceq 1633    e. wcel 1701   Ord word 4428
This theorem is referenced by:  ordunisuc2  4672  tz7.48lem  6495  oacan  6588  omcan  6609  oecan  6629  omsmo  6694  omopthi  6697  inf3lem6  7379  cantnfp1lem3  7427  infpssrlem5  7978  fin23lem24  7993  isf32lem4  8027  om2uzf1oi  11063  nodenselem4  24723
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-tr 4151  df-eprel 4342  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432
  Copyright terms: Public domain W3C validator