Theorem ontri1 6387

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 6386	. 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 2145   ⊆ wss 3899  Ord word 6351  Oncon0 6352

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5249  ax-pr 5391

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-ord 6355  df-on 6356

This theorem is used by:  oneqmini  6406  onmindif  6447  onint  7788  onnmin  7796  onmindif2  7805  dfom2  7863  ondif2  8489  oaword  8536  oawordeulem  8541  oaf1o  8550  odi  8566  omeulem1  8569  oeeulem  8589  oeeui  8590  nnmword  8621  cofonr  8662  naddel1  8676  naddss1  8678  domtriord  9121  sdomel  9122  onsdominel  9124  ordunifi  9260  cantnfp1lem3  9659  oemapvali  9663  cantnflem1b  9665  cantnflem1  9668  cnfcom3lem  9682  rankr1clem  9802  rankelb  9806  rankval3b  9808  rankr1a  9818  unbndrank  9825  rankxplim3  9867  cardne  10003  carden2b  10005  cardsdomel  10012  carddom2  10015  harcard  10016  domtri2  10027  infxpenlem  10049  alephord  10111  alephord3  10114  alephle  10124  dfac12k  10183  cflim2  10298  cofsmo  10304  cfsmolem  10305  isf32lem5  10392  pwcfsdom  10625  pwfseqlem3  10702  inar1  10817  om2uzlt2i  14048  ltsval2  27932  ltsres  27938  nosepssdm  27962  nolt02olem  27970  nolt02o  27971  nogt01o  27972  noetasuplem4  28012  noetainflem4  28016  nocvxminlem  28059  madebdaylemlrcut  28204  oncutlt  28569  onnolt  28571  onles  28573  oniso  28576  om2noseqlt2  28605  bdaypw2bnd  28770  bdayfinbndlem1  28772  nummin  35639  vonf1wev  35806  vonf1owevOLD  35808  ltnmul  36881  nmulle  36882  ltnadd  36883  naddle  36884  onsuct0  37145  onint1  37153  onmaxnelsup  44162  onsupnmax  44167  onsupuni  44168  oninfint  44175  onsupmaxb  44178  onsupeqnmax  44186  oe0suclim  44216  cantnfresb  44263  cantnf2  44264  tfsconcatfv  44280  tfsnfin  44291  oadif1lem  44318  oadif1  44319  naddwordnexlem4  44340  ontric3g  44460  infordmin  44470  minregex  44472  alephiso3  44497  hashnnltb  45944