Theorem ontri1 6396

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2149   ⊆ wss 3913  Ord word 6360  Oncon0 6361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-tr 5223  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-ord 6364  df-on 6365

This theorem is referenced by:  oneqmini  6415  onmindif  6456  onint  7789  onnmin  7797  onmindif2  7806  dfom2  7864  ondif2  8487  oaword  8534  oawordeulem  8539  oaf1o  8548  odi  8564  omeulem1  8567  oeeulem  8587  oeeui  8588  nnmword  8619  cofonr  8660  naddel1  8674  naddss1  8676  domtriord  9111  sdomel  9112  onsdominel  9114  ordunifi  9250  cantnfp1lem3  9649  oemapvali  9653  cantnflem1b  9655  cantnflem1  9658  cnfcom3lem  9672  rankr1clem  9792  rankelb  9796  rankval3b  9798  rankr1a  9808  unbndrank  9814  rankxplim3  9853  cardne  9951  carden2b  9953  cardsdomel  9960  carddom2  9963  harcard  9964  domtri2  9975  infxpenlem  9997  alephord  10059  alephord3  10062  alephle  10072  dfac12k  10131  cflim2  10247  cofsmo  10253  cfsmolem  10254  isf32lem5  10341  pwcfsdom  10568  pwfseqlem3  10645  inar1  10760  om2uzlt2i  13987  ltsval2  27786  ltsres  27792  nosepssdm  27816  nolt02olem  27824  nolt02o  27825  nogt01o  27826  noetasuplem4  27866  noetainflem4  27870  nocvxminlem  27913  madebdaylemlrcut  28058  oncutlt  28423  onnolt  28425  onles  28427  oniso  28430  om2noseqlt2  28459  bdaypw2bnd  28624  bdayfinbndlem1  28626  nummin  35427  vonf1wev  35525  vonf1owevOLD  35527  onsuct0  36875  onint1  36883  onmaxnelsup  43876  onsupnmax  43881  onsupuni  43882  oninfint  43889  onsupmaxb  43892  onsupeqnmax  43900  oe0suclim  43930  cantnfresb  43977  cantnf2  43978  tfsconcatfv  43994  tfsnfin  44005  oadif1lem  44032  oadif1  44033  naddwordnexlem4  44054  ontric3g  44174  infordmin  44184  minregex  44186  alephiso3  44211  hashnnltb  45658