Theorem ontri1 6397

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895  Ord word 6361  Oncon0 6362

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366

This theorem is used by:  oneqmini  6416  onmindif  6457  onint  7804  onnmin  7812  onmindif2  7821  dfom2  7879  ondif2  8510  oaword  8557  oawordeulem  8562  oaf1o  8571  odi  8587  omeulem1  8590  oeeulem  8610  oeeui  8611  nnmword  8642  cofonr  8683  naddel1  8697  naddss1  8699  domtriord  9142  sdomel  9143  onsdominel  9145  ordunifi  9281  cantnfp1lem3  9681  oemapvali  9685  cantnflem1b  9687  cantnflem1  9690  cnfcom3lem  9704  rankr1clem  9829  rankelb  9833  rankval3b  9836  rankr1a  9848  unbndrank  9855  rankxplim3  9898  cardne  10046  carden2b  10048  cardsdomel  10055  carddom2  10058  harcard  10059  domtri2  10070  infxpenlem  10092  alephord  10154  alephord3  10157  alephle  10167  dfac12k  10226  cflim2  10341  cofsmo  10347  cfsmolem  10348  isf32lem5  10435  pwcfsdom  10668  pwfseqlem3  10745  inar1  10860  om2uzlt2i  14094  ltsval2  28013  ltsres  28019  nosepssdm  28043  nolt02olem  28051  nolt02o  28052  nogt01o  28053  noetasuplem4  28093  noetainflem4  28097  nocvxminlem  28140  madebdaylemlrcut  28285  oncutlt  28650  onnolt  28652  onles  28654  oniso  28657  om2noseqlt2  28686  bdaypw2bnd  28851  bdayfinbndlem1  28853  nummin  35722  vonf1wev  35887  vonf1owevOLD  35889  onprcf1acwevdlem1  35895  ltnmul  36965  nmulle  36966  ltnadd  36967  naddle  36968  onsuct0  37229  onint1  37237  onmaxnelsup  44225  onsupnmax  44230  onsupuni  44231  oninfint  44238  onsupmaxb  44241  onsupeqnmax  44249  oe0suclim  44279  cantnfresb  44326  cantnf2  44327  tfsconcatfv  44343  tfsnfin  44354  oadif1lem  44381  oadif1  44382  naddwordnexlem4  44403  ontric3g  44523  infordmin  44533  minregex  44535  alephiso3  44560  hashnnltb  46013