Theorem endomtr 7974

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

Syntax hints:   → wi 4   ∧ wa 384   class class class wbr 4623   ≈ cen 7912   ≼ cdom 7913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-f1o 5864  df-en 7916  df-dom 7917

This theorem is referenced by:  cnvct  7993  undom  8008  xpdom1g  8017  xpdom3  8018  domunsncan  8020  domsdomtr  8055  domen1  8062  mapdom1  8085  mapdom2  8091  mapdom3  8092  php  8104  onomeneq  8110  sucdom2  8116  hartogslem1  8407  harcard  8764  infxpenlem  8796  infpwfien  8845  alephsucdom  8862  mappwen  8895  dfac12lem2  8926  cdalepw  8978  fictb  9027  cfflb  9041  canthp1lem1  9434  pwfseqlem5  9445  pwxpndom2  9447  pwcdandom  9449  gchxpidm  9451  gchhar  9461  tskinf  9551  inar1  9557  gruina  9600  rexpen  14901  mreexdomd  16250  hauspwdom  21244  rectbntr0  22575  rabfodom  29232  snct  29375  dya2iocct  30165  finminlem  32007  lindsdom  33074  poimirlem26  33106  heiborlem3  33283  pellexlem4  36915  pellexlem5  36916  mpct  38902  aacllem  41880