Theorem ontri1 6386

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 6362	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6362	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6385	. 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 3926  Ord word 6351  Oncon0 6352

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356

This theorem is referenced by:  oneqmini  6405  onmindif  6445  onint  7782  onnmin  7790  onmindif2  7799  dfom2  7861  ondif2  8512  oaword  8559  oawordeulem  8564  oaf1o  8573  odi  8589  omeulem1  8592  oeeulem  8611  oeeui  8612  nnmword  8643  cofonr  8684  naddel1  8697  naddss1  8699  domtriord  9135  sdomel  9136  onsdominel  9138  ordunifi  9296  cantnfp1lem3  9692  oemapvali  9696  cantnflem1b  9698  cantnflem1  9701  cnfcom3lem  9715  rankr1clem  9832  rankelb  9836  rankval3b  9838  rankr1a  9848  unbndrank  9854  rankxplim3  9893  cardne  9977  carden2b  9979  cardsdomel  9986  carddom2  9989  harcard  9990  domtri2  10001  infxpenlem  10025  alephord  10087  alephord3  10090  alephle  10100  dfac12k  10160  cflim2  10275  cofsmo  10281  cfsmolem  10282  isf32lem5  10369  pwcfsdom  10595  pwfseqlem3  10672  inar1  10787  om2uzlt2i  13967  sltval2  27618  sltres  27624  nosepssdm  27648  nolt02olem  27656  nolt02o  27657  nogt01o  27658  noetasuplem4  27698  noetainflem4  27702  nocvxminlem  27739  madebdaylemlrcut  27854  om2noseqlt2  28223  nummin  35068  onsuct0  36405  onint1  36413  onmaxnelsup  43194  onsupnmax  43199  onsupuni  43200  oninfint  43207  onsupmaxb  43210  onsupeqnmax  43218  oe0suclim  43248  cantnfresb  43295  cantnf2  43296  tfsconcatfv  43312  tfsnfin  43323  oadif1lem  43350  oadif1  43351  naddwordnexlem4  43372  ontric3g  43493  infordmin  43503  minregex  43505  alephiso3  43530