Theorem endomtr 8956

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 8923	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)
2		domtr 8951	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
3	1, 2	sylan 581	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5086   ≈ cen 8887   ≼ cdom 8888

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-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pow 5306  ax-pr 5374  ax-un 7686

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5523  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-f1o 6503  df-en 8891  df-dom 8892

This theorem is referenced by:  cnvct  8978  xpdom1g  9009  xpdom3  9010  domunsncan  9012  domsdomtr  9047  domen1  9054  mapdom1  9077  mapdom2  9083  mapdom3  9084  hartogslem1  9454  harcard  9899  infxpenlem  9932  infpwfien  9981  alephsucdom  9998  mappwen  10031  dfac12lem2  10064  djulepw  10112  fictb  10163  cfflb  10178  canthp1lem1  10572  pwfseqlem5  10583  pwxpndom2  10585  pwdjundom  10587  gchxpidm  10589  gchhar  10599  tskinf  10689  inar1  10695  gruina  10738  rexpen  16192  mreexdomd  17612  hauspwdom  23482  rectbntr0  24814  rabfodom  32596  snct  32806  dya2iocct  34446  finminlem  36522  iccioo01  37665  pibt2  37755  lindsdom  37957  poimirlem26  37989  heiborlem3  38156  pellexlem4  43286  pellexlem5  43287  safesnsupfidom1o  43870  sn1dom  43979  mpct  45656  thincciso2  49950  aacllem  50296