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 3911  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 5259  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 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  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  43877  onsupnmax  43882  onsupuni  43883  oninfint  43890  onsupmaxb  43893  onsupeqnmax  43901  oe0suclim  43931  cantnfresb  43978  cantnf2  43979  tfsconcatfv  43995  tfsnfin  44006  oadif1lem  44033  oadif1  44034  naddwordnexlem4  44055  ontric3g  44175  infordmin  44185  minregex  44187  alephiso3  44212  hashnnltb  45659