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

Theorem ontri1 5716
Description: A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.)
Assertion
Ref Expression
ontri1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐵 ↔ ¬ 𝐵𝐴))

Proof of Theorem ontri1
StepHypRef Expression
1 eloni 5692 . 2 (𝐴 ∈ On → Ord 𝐴)
2 eloni 5692 . 2 (𝐵 ∈ On → Ord 𝐵)
3 ordtri1 5715 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵 ↔ ¬ 𝐵𝐴))
41, 2, 3syl2an 494 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wcel 1987  wss 3555  Ord word 5681  Oncon0 5682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-tr 4713  df-eprel 4985  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-ord 5685  df-on 5686
This theorem is referenced by:  oneqmini  5735  onmindif  5774  onint  6942  onnmin  6950  onmindif2  6959  dfom2  7014  ondif2  7527  oaword  7574  oawordeulem  7579  oaf1o  7588  odi  7604  omeulem1  7607  oeeulem  7626  oeeui  7627  nnmword  7658  domtriord  8050  sdomel  8051  onsdominel  8053  ordunifi  8154  cantnfp1lem3  8521  oemapvali  8525  cantnflem1b  8527  cantnflem1  8530  cnfcom3lem  8544  rankr1clem  8627  rankelb  8631  rankval3b  8633  rankr1a  8643  unbndrank  8649  rankxplim3  8688  cardne  8735  carden2b  8737  cardsdomel  8744  carddom2  8747  harcard  8748  domtri2  8759  infxpenlem  8780  alephord  8842  alephord3  8845  alephle  8855  dfac12k  8913  cflim2  9029  cofsmo  9035  cfsmolem  9036  isf32lem5  9123  pwcfsdom  9349  pwfseqlem3  9426  inar1  9541  om2uzlt2i  12690  sltval2  31507  sltres  31515  nodenselem7  31547  nocvxminlem  31550  nobndup  31560  nobnddown  31561  onsuct0  32079  onint1  32087
  Copyright terms: Public domain W3C validator