Theorem endomtr 8951

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

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

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 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-f1o 6498  df-en 8886  df-dom 8887

This theorem is referenced by:  cnvct  8973  xpdom1g  9004  xpdom3  9005  domunsncan  9007  domsdomtr  9042  domen1  9049  mapdom1  9072  mapdom2  9078  mapdom3  9079  hartogslem1  9449  harcard  9892  infxpenlem  9925  infpwfien  9974  alephsucdom  9991  mappwen  10024  dfac12lem2  10057  djulepw  10105  fictb  10156  cfflb  10171  canthp1lem1  10565  pwfseqlem5  10576  pwxpndom2  10578  pwdjundom  10580  gchxpidm  10582  gchhar  10592  tskinf  10682  inar1  10688  gruina  10731  rexpen  16155  mreexdomd  17574  hauspwdom  23447  rectbntr0  24779  rabfodom  32560  snct  32770  dya2iocct  34416  finminlem  36491  iccioo01  37501  pibt2  37591  lindsdom  37784  poimirlem26  37816  heiborlem3  37983  pellexlem4  43111  pellexlem5  43112  safesnsupfidom1o  43695  sn1dom  43804  mpct  45482  thincciso2  49737  aacllem  50083