Theorem ontri1 6419

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2105   ⊆ wss 3962  Ord word 6384  Oncon0 6385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389

This theorem is referenced by:  oneqmini  6437  onmindif  6477  onint  7809  onnmin  7817  onmindif2  7826  dfom2  7888  ondif2  8538  oaword  8585  oawordeulem  8590  oaf1o  8599  odi  8615  omeulem1  8618  oeeulem  8637  oeeui  8638  nnmword  8669  cofonr  8710  naddel1  8723  naddss1  8725  domtriord  9161  sdomel  9162  onsdominel  9164  ordunifi  9323  cantnfp1lem3  9717  oemapvali  9721  cantnflem1b  9723  cantnflem1  9726  cnfcom3lem  9740  rankr1clem  9857  rankelb  9861  rankval3b  9863  rankr1a  9873  unbndrank  9879  rankxplim3  9918  cardne  10002  carden2b  10004  cardsdomel  10011  carddom2  10014  harcard  10015  domtri2  10026  infxpenlem  10050  alephord  10112  alephord3  10115  alephle  10125  dfac12k  10185  cflim2  10300  cofsmo  10306  cfsmolem  10307  isf32lem5  10394  pwcfsdom  10620  pwfseqlem3  10697  inar1  10812  om2uzlt2i  13988  sltval2  27715  sltres  27721  nosepssdm  27745  nolt02olem  27753  nolt02o  27754  nogt01o  27755  noetasuplem4  27795  noetainflem4  27799  nocvxminlem  27836  madebdaylemlrcut  27951  om2noseqlt2  28320  nummin  35083  onsuct0  36423  onint1  36431  onmaxnelsup  43211  onsupnmax  43216  onsupuni  43217  oninfint  43224  onsupmaxb  43227  onsupeqnmax  43235  oe0suclim  43266  cantnfresb  43313  cantnf2  43314  tfsconcatfv  43330  tfsnfin  43341  oadif1lem  43368  oadif1  43369  naddwordnexlem4  43390  ontric3g  43511  infordmin  43521  minregex  43523  alephiso3  43548