Theorem ontri1 6354

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 6330	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6330	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6353	. 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 3911  Ord word 6319  Oncon0 6320

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324

This theorem is referenced by:  oneqmini  6373  onmindif  6414  onint  7746  onnmin  7754  onmindif2  7763  dfom2  7824  ondif2  8443  oaword  8490  oawordeulem  8495  oaf1o  8504  odi  8520  omeulem1  8523  oeeulem  8542  oeeui  8543  nnmword  8574  cofonr  8615  naddel1  8628  naddss1  8630  domtriord  9064  sdomel  9065  onsdominel  9067  ordunifi  9213  cantnfp1lem3  9609  oemapvali  9613  cantnflem1b  9615  cantnflem1  9618  cnfcom3lem  9632  rankr1clem  9749  rankelb  9753  rankval3b  9755  rankr1a  9765  unbndrank  9771  rankxplim3  9810  cardne  9894  carden2b  9896  cardsdomel  9903  carddom2  9906  harcard  9907  domtri2  9918  infxpenlem  9942  alephord  10004  alephord3  10007  alephle  10017  dfac12k  10077  cflim2  10192  cofsmo  10198  cfsmolem  10199  isf32lem5  10286  pwcfsdom  10512  pwfseqlem3  10589  inar1  10704  om2uzlt2i  13892  sltval2  27601  sltres  27607  nosepssdm  27631  nolt02olem  27639  nolt02o  27640  nogt01o  27641  noetasuplem4  27681  noetainflem4  27685  nocvxminlem  27723  madebdaylemlrcut  27848  onscutlt  28205  onnolt  28207  onsiso  28209  om2noseqlt2  28234  nummin  35074  vonf1owev  35088  onsuct0  36422  onint1  36430  onmaxnelsup  43205  onsupnmax  43210  onsupuni  43211  oninfint  43218  onsupmaxb  43221  onsupeqnmax  43229  oe0suclim  43259  cantnfresb  43306  cantnf2  43307  tfsconcatfv  43323  tfsnfin  43334  oadif1lem  43361  oadif1  43362  naddwordnexlem4  43383  ontric3g  43504  infordmin  43514  minregex  43516  alephiso3  43541