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

Theorem ontri1 5910
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 5886 . 2 (𝐴 ∈ On → Ord 𝐴)
2 eloni 5886 . 2 (𝐵 ∈ On → Ord 𝐵)
3 ordtri1 5909 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴𝐵 ↔ ¬ 𝐵𝐴))
41, 2, 3syl2an 495 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wcel 2131  wss 3707  Ord word 5875  Oncon0 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-tr 4897  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-ord 5879  df-on 5880
This theorem is referenced by:  oneqmini  5929  onmindif  5968  onint  7152  onnmin  7160  onmindif2  7169  dfom2  7224  ondif2  7743  oaword  7790  oawordeulem  7795  oaf1o  7804  odi  7820  omeulem1  7823  oeeulem  7842  oeeui  7843  nnmword  7874  domtriord  8263  sdomel  8264  onsdominel  8266  ordunifi  8367  cantnfp1lem3  8742  oemapvali  8746  cantnflem1b  8748  cantnflem1  8751  cnfcom3lem  8765  rankr1clem  8848  rankelb  8852  rankval3b  8854  rankr1a  8864  unbndrank  8870  rankxplim3  8909  cardne  8973  carden2b  8975  cardsdomel  8982  carddom2  8985  harcard  8986  domtri2  8997  infxpenlem  9018  alephord  9080  alephord3  9083  alephle  9093  dfac12k  9153  cflim2  9269  cofsmo  9275  cfsmolem  9276  isf32lem5  9363  pwcfsdom  9589  pwfseqlem3  9666  inar1  9781  om2uzlt2i  12936  sltval2  32107  sltres  32113  nosepssdm  32134  nolt02olem  32142  nolt02o  32143  noetalem3  32163  nocvxminlem  32191  onsuct0  32738  onint1  32746
  Copyright terms: Public domain W3C validator