Theorem ontri1 6412

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900  Ord word 6376  Oncon0 6377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-tr 5216  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6380  df-on 6381

This theorem is used by:  oneqmini  6431  onmindif  6472  onint  7825  onnmin  7833  onmindif2  7842  dfom2  7900  ondif2  8535  oaword  8582  oawordeulem  8587  oaf1o  8596  odi  8612  omeulem1  8615  oeeulem  8635  oeeui  8636  nnmword  8667  cofonr  8708  naddel1  8722  naddss1  8724  domtriord  9167  sdomel  9168  onsdominel  9170  ordunifi  9306  cantnfp1lem3  9705  oemapvali  9709  cantnflem1b  9711  cantnflem1  9714  cnfcom3lem  9728  rankr1clem  9853  rankelb  9857  rankval3b  9860  rankr1a  9872  unbndrank  9879  rankxplim3  9922  cardne  10070  carden2b  10072  cardsdomel  10079  carddom2  10082  harcard  10083  domtri2  10094  infxpenlem  10116  alephord  10178  alephord3  10181  alephle  10191  dfac12k  10250  cflim2  10365  cofsmo  10371  cfsmolem  10372  isf32lem5  10459  pwcfsdom  10692  pwfseqlem3  10769  inar1  10884  om2uzlt2i  14118  ltsval2  28040  ltsres  28046  nosepssdm  28070  nolt02olem  28078  nolt02o  28079  nogt01o  28080  noetasuplem4  28120  noetainflem4  28124  nocvxminlem  28167  madebdaylemlrcut  28312  oncutlt  28677  onnolt  28679  onles  28681  oniso  28684  om2noseqlt2  28713  bdaypw2bnd  28878  bdayfinbndlem1  28880  nummin  35803  vonf1wev  36035  vonf1owevOLD  36037  onprcf1acwevdlem1  36044  ltnmul  37142  nmulle  37143  ltnadd  37144  naddle  37145  onsuct0  37406  onint1  37414  onmaxnelsup  44415  onsupnmax  44420  onsupuni  44421  oninfint  44428  onsupmaxb  44431  onsupeqnmax  44439  oe0suclim  44469  cantnfresb  44516  cantnf2  44517  tfsconcatfv  44533  tfsnfin  44544  oadif1lem  44571  oadif1  44572  naddwordnexlem4  44593  ontric3g  44713  infordmin  44723  minregex  44725  alephiso3  44750  hashnnltb  46206