Theorem endomtr 8937

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

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5092   ≈ cen 8869   ≼ cdom 8870

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-f1o 6489  df-en 8873  df-dom 8874

This theorem is referenced by:  cnvct  8959  xpdom1g  8991  xpdom3  8992  domunsncan  8994  domsdomtr  9029  domen1  9036  mapdom1  9059  mapdom2  9065  mapdom3  9066  hartogslem1  9434  harcard  9874  infxpenlem  9907  infpwfien  9956  alephsucdom  9973  mappwen  10006  dfac12lem2  10039  djulepw  10087  fictb  10138  cfflb  10153  canthp1lem1  10546  pwfseqlem5  10557  pwxpndom2  10559  pwdjundom  10561  gchxpidm  10563  gchhar  10573  tskinf  10663  inar1  10669  gruina  10712  rexpen  16137  mreexdomd  17555  hauspwdom  23386  rectbntr0  24719  rabfodom  32454  snct  32664  dya2iocct  34264  finminlem  36312  iccioo01  37321  pibt2  37411  lindsdom  37614  poimirlem26  37646  heiborlem3  37813  pellexlem4  42825  pellexlem5  42826  safesnsupfidom1o  43410  sn1dom  43519  mpct  45199  thincciso2  49460  aacllem  49806