Theorem sdomentr 9018

Description: Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98. (Contributed by NM, 26-Oct-2003.)

Assertion

Ref	Expression
sdomentr	⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≺ 𝐶)

Proof of Theorem sdomentr

Step	Hyp	Ref	Expression
1		endom 8895	. 2 ⊢ (𝐵 ≈ 𝐶 → 𝐵 ≼ 𝐶)
2		sdomdomtr 9017	. 2 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶)
3	1, 2	sylan2 593	1 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≺ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5088   ≈ cen 8860   ≼ cdom 8861   ≺ csdm 8862

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-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5367  ax-un 7662

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-id 5508  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-er 8616  df-en 8864  df-dom 8865  df-sdom 8866

This theorem is referenced by:  sdomen2  9029  unxpdom2  9138  sucxpdom  9139  fofinf1o  9210  sdomsdomcardi  9855  cardsdomel  9858  cardmin2  9883  alephnbtwn2  9954  pwsdompw  10085  infdif2  10091  fin23lem27  10210  axcclem  10339  numthcor  10376  sdomsdomcard  10442  pwcfsdom  10465  cfpwsdom  10466  inawinalem  10571  inatsk  10660  r1tskina  10664  tskuni  10665  rucALT  16126  iunmbl2  25439  dirith2  27420  erdszelem10  35190  mblfinlem1  37654  pellex  42825  rp-isfinite6  43508  harval3  43528