Theorem ontri1 6406

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∈ wcel 2098   ⊆ wss 3947  Ord word 6371  Oncon0 6372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-sep 5301  ax-nul 5308  ax-pr 5431

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-opab 5213  df-tr 5268  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-we 5637  df-ord 6375  df-on 6376

This theorem is referenced by:  oneqmini  6424  onmindif  6464  onint  7797  onnmin  7805  onmindif2  7814  dfom2  7876  ondif2  8527  oaword  8574  oawordeulem  8579  oaf1o  8588  odi  8604  omeulem1  8607  oeeulem  8626  oeeui  8627  nnmword  8658  cofonr  8699  naddel1  8712  naddss1  8714  domtriord  9152  sdomel  9153  onsdominel  9155  ordunifi  9322  cantnfp1lem3  9709  oemapvali  9713  cantnflem1b  9715  cantnflem1  9718  cnfcom3lem  9732  rankr1clem  9849  rankelb  9853  rankval3b  9855  rankr1a  9865  unbndrank  9871  rankxplim3  9910  cardne  9994  carden2b  9996  cardsdomel  10003  carddom2  10006  harcard  10007  domtri2  10018  infxpenlem  10042  alephord  10104  alephord3  10107  alephle  10117  dfac12k  10176  cflim2  10292  cofsmo  10298  cfsmolem  10299  isf32lem5  10386  pwcfsdom  10612  pwfseqlem3  10689  inar1  10804  om2uzlt2i  13954  sltval2  27607  sltres  27613  nosepssdm  27637  nolt02olem  27645  nolt02o  27646  nogt01o  27647  noetasuplem4  27687  noetainflem4  27691  nocvxminlem  27728  madebdaylemlrcut  27843  om2noseqlt2  28191  nummin  34719  onsuct0  35930  onint1  35938  onmaxnelsup  42654  onsupnmax  42659  onsupuni  42660  oninfint  42667  onsupmaxb  42670  onsupeqnmax  42678  oe0suclim  42709  cantnfresb  42756  cantnf2  42757  tfsconcatfv  42773  tfsnfin  42784  oadif1lem  42811  oadif1  42812  naddwordnexlem4  42834  ontric3g  42955  infordmin  42965  minregex  42967  alephiso3  42992