Theorem ontri1 6361

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3903  Ord word 6326  Oncon0 6327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-ord 6330  df-on 6331

This theorem is referenced by:  oneqmini  6380  onmindif  6421  onint  7747  onnmin  7755  onmindif2  7764  dfom2  7822  ondif2  8441  oaword  8488  oawordeulem  8493  oaf1o  8502  odi  8518  omeulem1  8521  oeeulem  8541  oeeui  8542  nnmword  8573  cofonr  8614  naddel1  8627  naddss1  8629  domtriord  9065  sdomel  9066  onsdominel  9068  ordunifi  9204  cantnfp1lem3  9603  oemapvali  9607  cantnflem1b  9609  cantnflem1  9612  cnfcom3lem  9626  rankr1clem  9746  rankelb  9750  rankval3b  9752  rankr1a  9762  unbndrank  9768  rankxplim3  9807  cardne  9891  carden2b  9893  cardsdomel  9900  carddom2  9903  harcard  9904  domtri2  9915  infxpenlem  9937  alephord  9999  alephord3  10002  alephle  10012  dfac12k  10072  cflim2  10187  cofsmo  10193  cfsmolem  10194  isf32lem5  10281  pwcfsdom  10508  pwfseqlem3  10585  inar1  10700  om2uzlt2i  13888  ltsval2  27641  ltsres  27647  nosepssdm  27671  nolt02olem  27679  nolt02o  27680  nogt01o  27681  noetasuplem4  27721  noetainflem4  27725  nocvxminlem  27767  madebdaylemlrcut  27912  oncutlt  28277  onnolt  28279  onles  28281  oniso  28284  om2noseqlt2  28313  bdaypw2bnd  28478  bdayfinbndlem1  28480  nummin  35276  vonf1owev  35330  onsuct0  36663  onint1  36671  onmaxnelsup  43609  onsupnmax  43614  onsupuni  43615  oninfint  43622  onsupmaxb  43625  onsupeqnmax  43633  oe0suclim  43663  cantnfresb  43710  cantnf2  43711  tfsconcatfv  43727  tfsnfin  43738  oadif1lem  43765  oadif1  43766  naddwordnexlem4  43787  ontric3g  43907  infordmin  43917  minregex  43919  alephiso3  43944