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

Theorem ontri1 4901
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 4877 . 2  |-  ( A  e.  On  ->  Ord  A )
2 eloni 4877 . 2  |-  ( B  e.  On  ->  Ord  B )
3 ordtri1 4900 . 2  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  C_  B  <->  -.  B  e.  A ) )
41, 2, 3syl2an 475 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 367    e. wcel 1823    C_ wss 3461   Ord word 4866   Oncon0 4867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-tr 4533  df-eprel 4780  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871
This theorem is referenced by:  oneqmini  4918  onmindif  4956  onint  6603  onnmin  6611  onmindif2  6620  dfom2  6675  ondif2  7144  oaword  7190  oawordeulem  7195  oaf1o  7204  odi  7220  omeulem1  7223  oeeulem  7242  oeeui  7243  nnmword  7274  domtriord  7656  sdomel  7657  onsdominel  7659  ordunifi  7762  cantnfp1lem3  8090  oemapvali  8094  cantnflem1b  8096  cantnflem1  8099  cantnfp1lem3OLD  8116  cantnflem1bOLD  8119  cantnflem1OLD  8122  cnfcom3lem  8138  cnfcom3lemOLD  8146  rankr1clem  8229  rankelb  8233  rankval3b  8235  rankr1a  8245  unbndrank  8251  rankxplim3  8290  cardne  8337  carden2b  8339  cardsdomel  8346  carddom2  8349  harcard  8350  domtri2  8361  infxpenlem  8382  alephord  8447  alephord3  8450  alephle  8460  dfac12k  8518  cflim2  8634  cofsmo  8640  cfsmolem  8641  isf32lem5  8728  pwcfsdom  8949  pwfseqlem3  9027  inar1  9142  om2uzlt2i  12044  sltval2  29656  sltres  29664  nodenselem7  29687  nocvxminlem  29690  nobndup  29700  nobnddown  29701  onsuct0  30134  onint1  30142
  Copyright terms: Public domain W3C validator