Theorem ontri1 6354

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 6330	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6330	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6353	. 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 3911  Ord word 6319  Oncon0 6320

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324

This theorem is referenced by:  oneqmini  6373  onmindif  6414  onint  7746  onnmin  7754  onmindif2  7763  dfom2  7824  ondif2  8443  oaword  8490  oawordeulem  8495  oaf1o  8504  odi  8520  omeulem1  8523  oeeulem  8542  oeeui  8543  nnmword  8574  cofonr  8615  naddel1  8628  naddss1  8630  domtriord  9064  sdomel  9065  onsdominel  9067  ordunifi  9213  cantnfp1lem3  9611  oemapvali  9615  cantnflem1b  9617  cantnflem1  9620  cnfcom3lem  9634  rankr1clem  9751  rankelb  9755  rankval3b  9757  rankr1a  9767  unbndrank  9773  rankxplim3  9812  cardne  9896  carden2b  9898  cardsdomel  9905  carddom2  9908  harcard  9909  domtri2  9920  infxpenlem  9944  alephord  10006  alephord3  10009  alephle  10019  dfac12k  10079  cflim2  10194  cofsmo  10200  cfsmolem  10201  isf32lem5  10288  pwcfsdom  10514  pwfseqlem3  10591  inar1  10706  om2uzlt2i  13894  sltval2  27602  sltres  27608  nosepssdm  27632  nolt02olem  27640  nolt02o  27641  nogt01o  27642  noetasuplem4  27682  noetainflem4  27686  nocvxminlem  27724  madebdaylemlrcut  27849  onscutlt  28206  onnolt  28208  onsiso  28210  om2noseqlt2  28235  nummin  35075  vonf1owev  35089  onsuct0  36423  onint1  36431  onmaxnelsup  43206  onsupnmax  43211  onsupuni  43212  oninfint  43219  onsupmaxb  43222  onsupeqnmax  43230  oe0suclim  43260  cantnfresb  43307  cantnf2  43308  tfsconcatfv  43324  tfsnfin  43335  oadif1lem  43362  oadif1  43363  naddwordnexlem4  43384  ontric3g  43505  infordmin  43515  minregex  43517  alephiso3  43542