Theorem ontri1 6429

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3976  Ord word 6394  Oncon0 6395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399

This theorem is referenced by:  oneqmini  6447  onmindif  6487  onint  7826  onnmin  7834  onmindif2  7843  dfom2  7905  ondif2  8558  oaword  8605  oawordeulem  8610  oaf1o  8619  odi  8635  omeulem1  8638  oeeulem  8657  oeeui  8658  nnmword  8689  cofonr  8730  naddel1  8743  naddss1  8745  domtriord  9189  sdomel  9190  onsdominel  9192  ordunifi  9354  cantnfp1lem3  9749  oemapvali  9753  cantnflem1b  9755  cantnflem1  9758  cnfcom3lem  9772  rankr1clem  9889  rankelb  9893  rankval3b  9895  rankr1a  9905  unbndrank  9911  rankxplim3  9950  cardne  10034  carden2b  10036  cardsdomel  10043  carddom2  10046  harcard  10047  domtri2  10058  infxpenlem  10082  alephord  10144  alephord3  10147  alephle  10157  dfac12k  10217  cflim2  10332  cofsmo  10338  cfsmolem  10339  isf32lem5  10426  pwcfsdom  10652  pwfseqlem3  10729  inar1  10844  om2uzlt2i  14002  sltval2  27719  sltres  27725  nosepssdm  27749  nolt02olem  27757  nolt02o  27758  nogt01o  27759  noetasuplem4  27799  noetainflem4  27803  nocvxminlem  27840  madebdaylemlrcut  27955  om2noseqlt2  28324  nummin  35067  onsuct0  36407  onint1  36415  onmaxnelsup  43184  onsupnmax  43189  onsupuni  43190  oninfint  43197  onsupmaxb  43200  onsupeqnmax  43208  oe0suclim  43239  cantnfresb  43286  cantnf2  43287  tfsconcatfv  43303  tfsnfin  43314  oadif1lem  43341  oadif1  43342  naddwordnexlem4  43363  ontric3g  43484  infordmin  43494  minregex  43496  alephiso3  43521