Theorem ontri1 6348

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 397   ∈ wcel 2121   ⊆ wss 3885  Ord word 6313  Oncon0 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-tr 5183  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318

This theorem is referenced by:  oneqmini  6367  onmindif  6408  onint  7737  onnmin  7745  onmindif2  7754  dfom2  7812  ondif2  8431  oaword  8478  oawordeulem  8483  oaf1o  8492  odi  8508  omeulem1  8511  oeeulem  8531  oeeui  8532  nnmword  8563  cofonr  8604  naddel1  8617  naddss1  8619  domtriord  9055  sdomel  9056  onsdominel  9058  ordunifi  9194  cantnfp1lem3  9596  oemapvali  9600  cantnflem1b  9602  cantnflem1  9605  cnfcom3lem  9619  rankr1clem  9739  rankelb  9743  rankval3b  9745  rankr1a  9755  unbndrank  9761  rankxplim3  9800  cardne  9884  carden2b  9886  cardsdomel  9893  carddom2  9896  harcard  9897  domtri2  9908  infxpenlem  9930  alephord  9992  alephord3  9995  alephle  10005  dfac12k  10065  cflim2  10180  cofsmo  10186  cfsmolem  10187  isf32lem5  10274  pwcfsdom  10501  pwfseqlem3  10578  inar1  10693  om2uzlt2i  13908  ltsval2  27642  ltsres  27648  nosepssdm  27672  nolt02olem  27680  nolt02o  27681  nogt01o  27682  noetasuplem4  27722  noetainflem4  27726  nocvxminlem  27768  madebdaylemlrcut  27913  oncutlt  28278  onnolt  28280  onles  28282  oniso  28285  om2noseqlt2  28314  bdaypw2bnd  28479  bdayfinbndlem1  28481  nummin  35289  vonf1owev  35351  onsuct0  36684  onint1  36692  onmaxnelsup  43683  onsupnmax  43688  onsupuni  43689  oninfint  43696  onsupmaxb  43699  onsupeqnmax  43707  oe0suclim  43737  cantnfresb  43784  cantnf2  43785  tfsconcatfv  43801  tfsnfin  43812  oadif1lem  43839  oadif1  43840  naddwordnexlem4  43861  ontric3g  43981  infordmin  43991  minregex  43993  alephiso3  44018