Theorem endomtr 9052

Description: Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)

Assertion

Ref	Expression
endomtr	⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Proof of Theorem endomtr

Step	Hyp	Ref	Expression
1		endom 9019	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)
2		domtr 9047	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
3	1, 2	sylan 580	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5143   ≈ cen 8982   ≼ cdom 8983

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-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-f1o 6568  df-en 8986  df-dom 8987

This theorem is referenced by:  cnvct  9074  undomOLD  9100  xpdom1g  9109  xpdom3  9110  domunsncan  9112  sucdom2OLD  9122  domsdomtr  9152  domen1  9159  mapdom1  9182  mapdom2  9188  mapdom3  9189  phpOLD  9259  onomeneqOLD  9266  hartogslem1  9582  harcard  10018  infxpenlem  10053  infpwfien  10102  alephsucdom  10119  mappwen  10152  dfac12lem2  10185  djulepw  10233  fictb  10284  cfflb  10299  canthp1lem1  10692  pwfseqlem5  10703  pwxpndom2  10705  pwdjundom  10707  gchxpidm  10709  gchhar  10719  tskinf  10809  inar1  10815  gruina  10858  rexpen  16264  mreexdomd  17692  hauspwdom  23509  rectbntr0  24854  rabfodom  32524  snct  32725  dya2iocct  34282  finminlem  36319  iccioo01  37328  pibt2  37418  lindsdom  37621  poimirlem26  37653  heiborlem3  37820  pellexlem4  42843  pellexlem5  42844  safesnsupfidom1o  43430  sn1dom  43539  mpct  45206  thincciso2  49104  aacllem  49320