Theorem ontri1 6382

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2144   ⊆ wss 3906  Ord word 6347  Oncon0 6348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-ord 6351  df-on 6352

This theorem is referenced by:  oneqmini  6401  onmindif  6442  onint  7775  onnmin  7783  onmindif2  7792  dfom2  7850  ondif2  8473  oaword  8520  oawordeulem  8525  oaf1o  8534  odi  8550  omeulem1  8553  oeeulem  8573  oeeui  8574  nnmword  8605  cofonr  8646  naddel1  8660  naddss1  8662  domtriord  9097  sdomel  9098  onsdominel  9100  ordunifi  9236  cantnfp1lem3  9637  oemapvali  9641  cantnflem1b  9643  cantnflem1  9646  cnfcom3lem  9660  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  9971  alephord  10033  alephord3  10036  alephle  10046  dfac12k  10106  cflim2  10222  cofsmo  10228  cfsmolem  10229  isf32lem5  10316  pwcfsdom  10543  pwfseqlem3  10620  inar1  10735  om2uzlt2i  13966  ltsval2  27722  ltsres  27728  nosepssdm  27752  nolt02olem  27760  nolt02o  27761  nogt01o  27762  noetasuplem4  27802  noetainflem4  27806  nocvxminlem  27849  madebdaylemlrcut  27994  oncutlt  28359  onnolt  28361  onles  28363  oniso  28366  om2noseqlt2  28395  bdaypw2bnd  28560  bdayfinbndlem1  28562  nummin  35391  vonf1wev  35455  vonf1owevOLD  35457  onsuct0  36806  onint1  36814  onmaxnelsup  43805  onsupnmax  43810  onsupuni  43811  oninfint  43818  onsupmaxb  43821  onsupeqnmax  43829  oe0suclim  43859  cantnfresb  43906  cantnf2  43907  tfsconcatfv  43923  tfsnfin  43934  oadif1lem  43961  oadif1  43962  naddwordnexlem4  43983  ontric3g  44103  infordmin  44113  minregex  44115  alephiso3  44140