Theorem ontri1 6352

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3902  Ord word 6317  Oncon0 6318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-tr 5207  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6321  df-on 6322

This theorem is referenced by:  oneqmini  6371  onmindif  6412  onint  7737  onnmin  7745  onmindif2  7754  dfom2  7812  ondif2  8431  oaword  8478  oawordeulem  8483  oaf1o  8492  odi  8508  omeulem1  8511  oeeulem  8531  oeeui  8532  nnmword  8563  cofonr  8604  naddel1  8617  naddss1  8619  domtriord  9055  sdomel  9056  onsdominel  9058  ordunifi  9194  cantnfp1lem3  9593  oemapvali  9597  cantnflem1b  9599  cantnflem1  9602  cnfcom3lem  9616  rankr1clem  9736  rankelb  9740  rankval3b  9742  rankr1a  9752  unbndrank  9758  rankxplim3  9797  cardne  9881  carden2b  9883  cardsdomel  9890  carddom2  9893  harcard  9894  domtri2  9905  infxpenlem  9927  alephord  9989  alephord3  9992  alephle  10002  dfac12k  10062  cflim2  10177  cofsmo  10183  cfsmolem  10184  isf32lem5  10271  pwcfsdom  10498  pwfseqlem3  10575  inar1  10690  om2uzlt2i  13878  ltsval2  27628  ltsres  27634  nosepssdm  27658  nolt02olem  27666  nolt02o  27667  nogt01o  27668  noetasuplem4  27708  noetainflem4  27712  nocvxminlem  27754  madebdaylemlrcut  27899  oncutlt  28264  onnolt  28266  onles  28268  oniso  28271  om2noseqlt2  28300  bdaypw2bnd  28465  bdayfinbndlem1  28467  nummin  35251  vonf1owev  35304  onsuct0  36637  onint1  36645  onmaxnelsup  43532  onsupnmax  43537  onsupuni  43538  oninfint  43545  onsupmaxb  43548  onsupeqnmax  43556  oe0suclim  43586  cantnfresb  43633  cantnf2  43634  tfsconcatfv  43650  tfsnfin  43661  oadif1lem  43688  oadif1  43689  naddwordnexlem4  43710  ontric3g  43830  infordmin  43840  minregex  43842  alephiso3  43867