Theorem ontri1 6395

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2142   ⊆ wss 3904  Ord word 6359  Oncon0 6360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-tr 5218  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-ord 6363  df-on 6364

This theorem is used by:  oneqmini  6414  onmindif  6455  onint  7787  onnmin  7795  onmindif2  7804  dfom2  7862  ondif2  8485  oaword  8532  oawordeulem  8537  oaf1o  8546  odi  8562  omeulem1  8565  oeeulem  8585  oeeui  8586  nnmword  8617  cofonr  8658  naddel1  8672  naddss1  8674  domtriord  9109  sdomel  9110  onsdominel  9112  ordunifi  9248  cantnfp1lem3  9647  oemapvali  9651  cantnflem1b  9653  cantnflem1  9656  cnfcom3lem  9670  rankr1clem  9790  rankelb  9794  rankval3b  9796  rankr1a  9806  unbndrank  9812  rankxplim3  9851  cardne  9958  carden2b  9960  cardsdomel  9967  carddom2  9970  harcard  9971  domtri2  9982  infxpenlem  10004  alephord  10066  alephord3  10069  alephle  10079  dfac12k  10138  cflim2  10253  cofsmo  10259  cfsmolem  10260  isf32lem5  10347  pwcfsdom  10574  pwfseqlem3  10651  inar1  10766  om2uzlt2i  13994  ltsval2  27831  ltsres  27837  nosepssdm  27861  nolt02olem  27869  nolt02o  27870  nogt01o  27871  noetasuplem4  27911  noetainflem4  27915  nocvxminlem  27958  madebdaylemlrcut  28103  oncutlt  28468  onnolt  28470  onles  28472  oniso  28475  om2noseqlt2  28504  bdaypw2bnd  28669  bdayfinbndlem1  28671  nummin  35493  vonf1wev  35600  vonf1owevOLD  35602  ltnmul  36716  nmulle  36717  ltnadd  36718  naddle  36719  onsuct0  36980  onint1  36988  onmaxnelsup  43978  onsupnmax  43983  onsupuni  43984  oninfint  43991  onsupmaxb  43994  onsupeqnmax  44002  oe0suclim  44032  cantnfresb  44079  cantnf2  44080  tfsconcatfv  44096  tfsnfin  44107  oadif1lem  44134  oadif1  44135  naddwordnexlem4  44156  ontric3g  44276  infordmin  44286  minregex  44288  alephiso3  44313  hashnnltb  45760