Theorem endomtr 9039

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   class class class wbr 5102   ≈ cen 8970   ≼ cdom 8971

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-f1o 6545  df-en 8974  df-dom 8975

This theorem is used by:  cnvct  9062  xpdom1g  9093  xpdom3  9094  domunsncan  9096  domsdomtr  9131  domen1  9138  mapdom1  9161  mapdom2  9167  mapdom3  9168  hartogslem1  9536  harcard  10059  infxpenlem  10092  infpwfien  10141  alephsucdom  10158  mappwen  10191  dfac12lem2  10223  djulepw  10271  fictb  10322  cfflb  10337  canthp1lem1  10737  pwfseqlem5  10748  pwxpndom2  10750  pwdjundom  10752  gchxpidm  10754  gchhar  10764  tskinf  10854  inar1  10860  gruina  10903  rexpen  16396  mreexdomd  17823  lindsdom  22156  hauspwdom  23820  rectbntr0  25152  rabfodom  33101  snct  33305  dya2iocct  34912  soinfdom  35717  karddom  35829  finminlem  37106  iccioo01  38251  pibt2  38341  poimirlem26  38565  heiborlem3  38748  pellexlem4  43839  pellexlem5  43840  safesnsupfidom1o  44418  sn1dom  44527  mpct  46215  thincciso2  50563  aacllem  50939