Theorem ontri1 6341

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3903  Ord word 6306  Oncon0 6307

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-tr 5200  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311

This theorem is referenced by:  oneqmini  6360  onmindif  6401  onint  7726  onnmin  7734  onmindif2  7743  dfom2  7801  ondif2  8420  oaword  8467  oawordeulem  8472  oaf1o  8481  odi  8497  omeulem1  8500  oeeulem  8519  oeeui  8520  nnmword  8551  cofonr  8592  naddel1  8605  naddss1  8607  domtriord  9040  sdomel  9041  onsdominel  9043  ordunifi  9179  cantnfp1lem3  9576  oemapvali  9580  cantnflem1b  9582  cantnflem1  9585  cnfcom3lem  9599  rankr1clem  9716  rankelb  9720  rankval3b  9722  rankr1a  9732  unbndrank  9738  rankxplim3  9777  cardne  9861  carden2b  9863  cardsdomel  9870  carddom2  9873  harcard  9874  domtri2  9885  infxpenlem  9907  alephord  9969  alephord3  9972  alephle  9982  dfac12k  10042  cflim2  10157  cofsmo  10163  cfsmolem  10164  isf32lem5  10251  pwcfsdom  10477  pwfseqlem3  10554  inar1  10669  om2uzlt2i  13858  sltval2  27566  sltres  27572  nosepssdm  27596  nolt02olem  27604  nolt02o  27605  nogt01o  27606  noetasuplem4  27646  noetainflem4  27650  nocvxminlem  27688  madebdaylemlrcut  27815  onscutlt  28172  onnolt  28174  onsiso  28176  om2noseqlt2  28201  nummin  35074  vonf1owev  35101  onsuct0  36435  onint1  36443  onmaxnelsup  43216  onsupnmax  43221  onsupuni  43222  oninfint  43229  onsupmaxb  43232  onsupeqnmax  43240  oe0suclim  43270  cantnfresb  43317  cantnf2  43318  tfsconcatfv  43334  tfsnfin  43345  oadif1lem  43372  oadif1  43373  naddwordnexlem4  43394  ontric3g  43515  infordmin  43525  minregex  43527  alephiso3  43552