Theorem endomtr 8179

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

Syntax hints:   → wi 4   ∧ wa 383   class class class wbr 4804   ≈ cen 8118   ≼ cdom 8119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-f1o 6056  df-en 8122  df-dom 8123

This theorem is referenced by:  cnvct  8198  undom  8213  xpdom1g  8222  xpdom3  8223  domunsncan  8225  domsdomtr  8260  domen1  8267  mapdom1  8290  mapdom2  8296  mapdom3  8297  php  8309  onomeneq  8315  sucdom2  8321  hartogslem1  8612  harcard  8994  infxpenlem  9026  infpwfien  9075  alephsucdom  9092  mappwen  9125  dfac12lem2  9158  cdalepw  9210  fictb  9259  cfflb  9273  canthp1lem1  9666  pwfseqlem5  9677  pwxpndom2  9679  pwcdandom  9681  gchxpidm  9683  gchhar  9693  tskinf  9783  inar1  9789  gruina  9832  rexpen  15156  mreexdomd  16511  hauspwdom  21506  rectbntr0  22836  rabfodom  29651  snct  29800  dya2iocct  30651  finminlem  32618  lindsdom  33716  poimirlem26  33748  heiborlem3  33925  pellexlem4  37898  pellexlem5  37899  mpct  39892  aacllem  43060