Theorem ontri1 6340

Description: A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.)

Assertion

Ref	Expression
ontri1	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Proof of Theorem ontri1

Step	Hyp	Ref	Expression
1		eloni 6316	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6316	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6339	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
4	1, 2, 3	syl2an 596	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2111   ⊆ wss 3897  Ord word 6305  Oncon0 6306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-tr 5197  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6309  df-on 6310

This theorem is referenced by:  oneqmini  6359  onmindif  6400  onint  7723  onnmin  7731  onmindif2  7740  dfom2  7798  ondif2  8417  oaword  8464  oawordeulem  8469  oaf1o  8478  odi  8494  omeulem1  8497  oeeulem  8516  oeeui  8517  nnmword  8548  cofonr  8589  naddel1  8602  naddss1  8604  domtriord  9036  sdomel  9037  onsdominel  9039  ordunifi  9174  cantnfp1lem3  9570  oemapvali  9574  cantnflem1b  9576  cantnflem1  9579  cnfcom3lem  9593  rankr1clem  9713  rankelb  9717  rankval3b  9719  rankr1a  9729  unbndrank  9735  rankxplim3  9774  cardne  9858  carden2b  9860  cardsdomel  9867  carddom2  9870  harcard  9871  domtri2  9882  infxpenlem  9904  alephord  9966  alephord3  9969  alephle  9979  dfac12k  10039  cflim2  10154  cofsmo  10160  cfsmolem  10161  isf32lem5  10248  pwcfsdom  10474  pwfseqlem3  10551  inar1  10666  om2uzlt2i  13858  sltval2  27595  sltres  27601  nosepssdm  27625  nolt02olem  27633  nolt02o  27634  nogt01o  27635  noetasuplem4  27675  noetainflem4  27679  nocvxminlem  27717  madebdaylemlrcut  27844  onscutlt  28201  onnolt  28203  onsiso  28205  om2noseqlt2  28230  nummin  35104  vonf1owev  35152  onsuct0  36485  onint1  36493  onmaxnelsup  43315  onsupnmax  43320  onsupuni  43321  oninfint  43328  onsupmaxb  43331  onsupeqnmax  43339  oe0suclim  43369  cantnfresb  43416  cantnf2  43417  tfsconcatfv  43433  tfsnfin  43444  oadif1lem  43471  oadif1  43472  naddwordnexlem4  43493  ontric3g  43614  infordmin  43624  minregex  43626  alephiso3  43651