Theorem ontri1 6366

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 6342	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6342	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6365	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
4	1, 2, 3	syl2an 596	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3914  Ord word 6331  Oncon0 6332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336

This theorem is referenced by:  oneqmini  6385  onmindif  6426  onint  7766  onnmin  7774  onmindif2  7783  dfom2  7844  ondif2  8466  oaword  8513  oawordeulem  8518  oaf1o  8527  odi  8543  omeulem1  8546  oeeulem  8565  oeeui  8566  nnmword  8597  cofonr  8638  naddel1  8651  naddss1  8653  domtriord  9087  sdomel  9088  onsdominel  9090  ordunifi  9237  cantnfp1lem3  9633  oemapvali  9637  cantnflem1b  9639  cantnflem1  9642  cnfcom3lem  9656  rankr1clem  9773  rankelb  9777  rankval3b  9779  rankr1a  9789  unbndrank  9795  rankxplim3  9834  cardne  9918  carden2b  9920  cardsdomel  9927  carddom2  9930  harcard  9931  domtri2  9942  infxpenlem  9966  alephord  10028  alephord3  10031  alephle  10041  dfac12k  10101  cflim2  10216  cofsmo  10222  cfsmolem  10223  isf32lem5  10310  pwcfsdom  10536  pwfseqlem3  10613  inar1  10728  om2uzlt2i  13916  sltval2  27568  sltres  27574  nosepssdm  27598  nolt02olem  27606  nolt02o  27607  nogt01o  27608  noetasuplem4  27648  noetainflem4  27652  nocvxminlem  27689  madebdaylemlrcut  27810  onscutlt  28165  onnolt  28167  onsiso  28169  om2noseqlt2  28194  nummin  35081  vonf1owev  35095  onsuct0  36429  onint1  36437  onmaxnelsup  43212  onsupnmax  43217  onsupuni  43218  oninfint  43225  onsupmaxb  43228  onsupeqnmax  43236  oe0suclim  43266  cantnfresb  43313  cantnf2  43314  tfsconcatfv  43330  tfsnfin  43341  oadif1lem  43368  oadif1  43369  naddwordnexlem4  43390  ontric3g  43511  infordmin  43521  minregex  43523  alephiso3  43548