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

Theorem ontri1 4753
Description: A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.)
Assertion
Ref Expression
ontri1  |-  ( ( A  e.  On  /\  B  e.  On )  ->  ( A  C_  B  <->  -.  B  e.  A ) )

Proof of Theorem ontri1
StepHypRef Expression
1 eloni 4729 . 2  |-  ( A  e.  On  ->  Ord  A )
2 eloni 4729 . 2  |-  ( B  e.  On  ->  Ord  B )
3 ordtri1 4752 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  C_  B  <->  -.  B  e.  A ) )
41, 2, 3syl2an 477 1  |-  ( ( A  e.  On  /\  B  e.  On )  ->  ( A  C_  B  <->  -.  B  e.  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1756    C_ wss 3328   Ord word 4718   Oncon0 4719
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 4413  ax-nul 4421  ax-pr 4531
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 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-tr 4386  df-eprel 4632  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723
This theorem is referenced by:  oneqmini  4770  onmindif  4808  onint  6406  onnmin  6414  onmindif2  6423  dfom2  6478  ondif2  6942  oaword  6988  oawordeulem  6993  oaf1o  7002  odi  7018  omeulem1  7021  oeeulem  7040  oeeui  7041  nnmword  7072  domtriord  7457  sdomel  7458  onsdominel  7460  ordunifi  7562  cantnfp1lem3  7888  oemapvali  7892  cantnflem1b  7894  cantnflem1  7897  cantnfp1lem3OLD  7914  cantnflem1bOLD  7917  cantnflem1OLD  7920  cnfcom3lem  7936  cnfcom3lemOLD  7944  rankr1clem  8027  rankelb  8031  rankval3b  8033  rankr1a  8043  unbndrank  8049  rankxplim3  8088  cardne  8135  carden2b  8137  cardsdomel  8144  carddom2  8147  harcard  8148  domtri2  8159  infxpenlem  8180  alephord  8245  alephord3  8248  alephle  8258  dfac12k  8316  cflim2  8432  cofsmo  8438  cfsmolem  8439  isf32lem5  8526  pwcfsdom  8747  pwfseqlem3  8827  inar1  8942  om2uzlt2i  11774  sltval2  27797  sltres  27805  nodenselem7  27828  nocvxminlem  27831  nobndup  27841  nobnddown  27842  onsuct0  28287  onint1  28295
  Copyright terms: Public domain W3C validator