Theorem ontri1 6350

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 6326	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6326	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6349	. 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 3900  Ord word 6315  Oncon0 6316

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 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376

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 2714  df-cleq 2727  df-clel 2810  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-tr 5205  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6319  df-on 6320

This theorem is referenced by:  oneqmini  6369  onmindif  6410  onint  7735  onnmin  7743  onmindif2  7752  dfom2  7810  ondif2  8429  oaword  8476  oawordeulem  8481  oaf1o  8490  odi  8506  omeulem1  8509  oeeulem  8529  oeeui  8530  nnmword  8561  cofonr  8602  naddel1  8615  naddss1  8617  domtriord  9053  sdomel  9054  onsdominel  9056  ordunifi  9192  cantnfp1lem3  9591  oemapvali  9595  cantnflem1b  9597  cantnflem1  9600  cnfcom3lem  9614  rankr1clem  9734  rankelb  9738  rankval3b  9740  rankr1a  9750  unbndrank  9756  rankxplim3  9795  cardne  9879  carden2b  9881  cardsdomel  9888  carddom2  9891  harcard  9892  domtri2  9903  infxpenlem  9925  alephord  9987  alephord3  9990  alephle  10000  dfac12k  10060  cflim2  10175  cofsmo  10181  cfsmolem  10182  isf32lem5  10269  pwcfsdom  10496  pwfseqlem3  10573  inar1  10688  om2uzlt2i  13876  sltval2  27626  sltres  27632  nosepssdm  27656  nolt02olem  27664  nolt02o  27665  nogt01o  27666  noetasuplem4  27706  noetainflem4  27710  nocvxminlem  27752  madebdaylemlrcut  27879  onscutlt  28243  onnolt  28245  onsle  28247  onsiso  28250  om2noseqlt2  28279  bdaypw2bnd  28442  bdayfinbndlem1  28444  nummin  35228  vonf1owev  35281  onsuct0  36614  onint1  36622  onmaxnelsup  43502  onsupnmax  43507  onsupuni  43508  oninfint  43515  onsupmaxb  43518  onsupeqnmax  43526  oe0suclim  43556  cantnfresb  43603  cantnf2  43604  tfsconcatfv  43620  tfsnfin  43631  oadif1lem  43658  oadif1  43659  naddwordnexlem4  43680  ontric3g  43800  infordmin  43810  minregex  43812  alephiso3  43837