Theorem endomtr 8950

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

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

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 5231  ax-pow 5300  ax-pr 5368  ax-un 7680

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 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-f1o 6497  df-en 8885  df-dom 8886

This theorem is referenced by:  cnvct  8972  xpdom1g  9003  xpdom3  9004  domunsncan  9006  domsdomtr  9041  domen1  9048  mapdom1  9071  mapdom2  9077  mapdom3  9078  hartogslem1  9448  harcard  9891  infxpenlem  9924  infpwfien  9973  alephsucdom  9990  mappwen  10023  dfac12lem2  10056  djulepw  10104  fictb  10155  cfflb  10170  canthp1lem1  10564  pwfseqlem5  10575  pwxpndom2  10577  pwdjundom  10579  gchxpidm  10581  gchhar  10591  tskinf  10681  inar1  10687  gruina  10730  rexpen  16184  mreexdomd  17604  hauspwdom  23475  rectbntr0  24807  rabfodom  32595  snct  32805  dya2iocct  34445  finminlem  36521  iccioo01  37654  pibt2  37744  lindsdom  37946  poimirlem26  37978  heiborlem3  38145  pellexlem4  43275  pellexlem5  43276  safesnsupfidom1o  43859  sn1dom  43968  mpct  45645  thincciso2  49927  aacllem  50273