Theorem ontri1 6357

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 6333	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6333	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6356	. 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 3889  Ord word 6322  Oncon0 6323

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327

This theorem is referenced by:  oneqmini  6376  onmindif  6417  onint  7744  onnmin  7752  onmindif2  7761  dfom2  7819  ondif2  8437  oaword  8484  oawordeulem  8489  oaf1o  8498  odi  8514  omeulem1  8517  oeeulem  8537  oeeui  8538  nnmword  8569  cofonr  8610  naddel1  8623  naddss1  8625  domtriord  9061  sdomel  9062  onsdominel  9064  ordunifi  9200  cantnfp1lem3  9601  oemapvali  9605  cantnflem1b  9607  cantnflem1  9610  cnfcom3lem  9624  rankr1clem  9744  rankelb  9748  rankval3b  9750  rankr1a  9760  unbndrank  9766  rankxplim3  9805  cardne  9889  carden2b  9891  cardsdomel  9898  carddom2  9901  harcard  9902  domtri2  9913  infxpenlem  9935  alephord  9997  alephord3  10000  alephle  10010  dfac12k  10070  cflim2  10185  cofsmo  10191  cfsmolem  10192  isf32lem5  10279  pwcfsdom  10506  pwfseqlem3  10583  inar1  10698  om2uzlt2i  13913  ltsval2  27620  ltsres  27626  nosepssdm  27650  nolt02olem  27658  nolt02o  27659  nogt01o  27660  noetasuplem4  27700  noetainflem4  27704  nocvxminlem  27746  madebdaylemlrcut  27891  oncutlt  28256  onnolt  28258  onles  28260  oniso  28263  om2noseqlt2  28292  bdaypw2bnd  28457  bdayfinbndlem1  28459  nummin  35236  vonf1owev  35290  onsuct0  36623  onint1  36631  onmaxnelsup  43651  onsupnmax  43656  onsupuni  43657  oninfint  43664  onsupmaxb  43667  onsupeqnmax  43675  oe0suclim  43705  cantnfresb  43752  cantnf2  43753  tfsconcatfv  43769  tfsnfin  43780  oadif1lem  43807  oadif1  43808  naddwordnexlem4  43829  ontric3g  43949  infordmin  43959  minregex  43961  alephiso3  43986