Theorem endomtr 8948

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

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5074   ≈ cen 8879   ≼ cdom 8880

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 2184  ax-ext 2707  ax-sep 5220  ax-pow 5296  ax-pr 5364  ax-un 7678

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-f1o 6494  df-en 8883  df-dom 8884

This theorem is referenced by:  cnvct  8970  xpdom1g  9001  xpdom3  9002  domunsncan  9004  domsdomtr  9039  domen1  9046  mapdom1  9069  mapdom2  9075  mapdom3  9076  hartogslem1  9446  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  23454  rectbntr0  24786  rabfodom  32563  snct  32773  dya2iocct  34412  finminlem  36488  iccioo01  37631  pibt2  37721  lindsdom  37923  poimirlem26  37955  heiborlem3  38122  pellexlem4  43248  pellexlem5  43249  safesnsupfidom1o  43832  sn1dom  43941  mpct  45618  thincciso2  49918  aacllem  50264