Theorem ontri1 6353

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 6329	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6329	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6352	. 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 3890  Ord word 6318  Oncon0 6319

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 5232  ax-pr 5372

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-ord 6322  df-on 6323

This theorem is referenced by:  oneqmini  6372  onmindif  6413  onint  7739  onnmin  7747  onmindif2  7756  dfom2  7814  ondif2  8432  oaword  8479  oawordeulem  8484  oaf1o  8493  odi  8509  omeulem1  8512  oeeulem  8532  oeeui  8533  nnmword  8564  cofonr  8605  naddel1  8618  naddss1  8620  domtriord  9056  sdomel  9057  onsdominel  9059  ordunifi  9195  cantnfp1lem3  9596  oemapvali  9600  cantnflem1b  9602  cantnflem1  9605  cnfcom3lem  9619  rankr1clem  9739  rankelb  9743  rankval3b  9745  rankr1a  9755  unbndrank  9761  rankxplim3  9800  cardne  9884  carden2b  9886  cardsdomel  9893  carddom2  9896  harcard  9897  domtri2  9908  infxpenlem  9930  alephord  9992  alephord3  9995  alephle  10005  dfac12k  10065  cflim2  10180  cofsmo  10186  cfsmolem  10187  isf32lem5  10274  pwcfsdom  10501  pwfseqlem3  10578  inar1  10693  om2uzlt2i  13908  ltsval2  27638  ltsres  27644  nosepssdm  27668  nolt02olem  27676  nolt02o  27677  nogt01o  27678  noetasuplem4  27718  noetainflem4  27722  nocvxminlem  27764  madebdaylemlrcut  27909  oncutlt  28274  onnolt  28276  onles  28278  oniso  28281  om2noseqlt2  28310  bdaypw2bnd  28475  bdayfinbndlem1  28477  nummin  35256  vonf1owev  35310  onsuct0  36643  onint1  36651  onmaxnelsup  43675  onsupnmax  43680  onsupuni  43681  oninfint  43688  onsupmaxb  43691  onsupeqnmax  43699  oe0suclim  43729  cantnfresb  43776  cantnf2  43777  tfsconcatfv  43793  tfsnfin  43804  oadif1lem  43831  oadif1  43832  naddwordnexlem4  43853  ontric3g  43973  infordmin  43983  minregex  43985  alephiso3  44010