Theorem ontri1 6418

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3951  Ord word 6383  Oncon0 6384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388

This theorem is referenced by:  oneqmini  6436  onmindif  6476  onint  7810  onnmin  7818  onmindif2  7827  dfom2  7889  ondif2  8540  oaword  8587  oawordeulem  8592  oaf1o  8601  odi  8617  omeulem1  8620  oeeulem  8639  oeeui  8640  nnmword  8671  cofonr  8712  naddel1  8725  naddss1  8727  domtriord  9163  sdomel  9164  onsdominel  9166  ordunifi  9326  cantnfp1lem3  9720  oemapvali  9724  cantnflem1b  9726  cantnflem1  9729  cnfcom3lem  9743  rankr1clem  9860  rankelb  9864  rankval3b  9866  rankr1a  9876  unbndrank  9882  rankxplim3  9921  cardne  10005  carden2b  10007  cardsdomel  10014  carddom2  10017  harcard  10018  domtri2  10029  infxpenlem  10053  alephord  10115  alephord3  10118  alephle  10128  dfac12k  10188  cflim2  10303  cofsmo  10309  cfsmolem  10310  isf32lem5  10397  pwcfsdom  10623  pwfseqlem3  10700  inar1  10815  om2uzlt2i  13992  sltval2  27701  sltres  27707  nosepssdm  27731  nolt02olem  27739  nolt02o  27740  nogt01o  27741  noetasuplem4  27781  noetainflem4  27785  nocvxminlem  27822  madebdaylemlrcut  27937  om2noseqlt2  28306  nummin  35105  onsuct0  36442  onint1  36450  onmaxnelsup  43235  onsupnmax  43240  onsupuni  43241  oninfint  43248  onsupmaxb  43251  onsupeqnmax  43259  oe0suclim  43290  cantnfresb  43337  cantnf2  43338  tfsconcatfv  43354  tfsnfin  43365  oadif1lem  43392  oadif1  43393  naddwordnexlem4  43414  ontric3g  43535  infordmin  43545  minregex  43547  alephiso3  43572