Theorem ontri1 6369

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 6345	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6345	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6368	. 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 3917  Ord word 6334  Oncon0 6335

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339

This theorem is referenced by:  oneqmini  6388  onmindif  6429  onint  7769  onnmin  7777  onmindif2  7786  dfom2  7847  ondif2  8469  oaword  8516  oawordeulem  8521  oaf1o  8530  odi  8546  omeulem1  8549  oeeulem  8568  oeeui  8569  nnmword  8600  cofonr  8641  naddel1  8654  naddss1  8656  domtriord  9093  sdomel  9094  onsdominel  9096  ordunifi  9244  cantnfp1lem3  9640  oemapvali  9644  cantnflem1b  9646  cantnflem1  9649  cnfcom3lem  9663  rankr1clem  9780  rankelb  9784  rankval3b  9786  rankr1a  9796  unbndrank  9802  rankxplim3  9841  cardne  9925  carden2b  9927  cardsdomel  9934  carddom2  9937  harcard  9938  domtri2  9949  infxpenlem  9973  alephord  10035  alephord3  10038  alephle  10048  dfac12k  10108  cflim2  10223  cofsmo  10229  cfsmolem  10230  isf32lem5  10317  pwcfsdom  10543  pwfseqlem3  10620  inar1  10735  om2uzlt2i  13923  sltval2  27575  sltres  27581  nosepssdm  27605  nolt02olem  27613  nolt02o  27614  nogt01o  27615  noetasuplem4  27655  noetainflem4  27659  nocvxminlem  27696  madebdaylemlrcut  27817  onscutlt  28172  onnolt  28174  onsiso  28176  om2noseqlt2  28201  nummin  35088  vonf1owev  35102  onsuct0  36436  onint1  36444  onmaxnelsup  43219  onsupnmax  43224  onsupuni  43225  oninfint  43232  onsupmaxb  43235  onsupeqnmax  43243  oe0suclim  43273  cantnfresb  43320  cantnf2  43321  tfsconcatfv  43337  tfsnfin  43348  oadif1lem  43375  oadif1  43376  naddwordnexlem4  43397  ontric3g  43518  infordmin  43528  minregex  43530  alephiso3  43555