Theorem endomtr 9018

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   class class class wbr 5103   ≈ cen 8949   ≼ cdom 8950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  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-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-f1o 6535  df-en 8953  df-dom 8954

This theorem is used by:  cnvct  9041  xpdom1g  9072  xpdom3  9073  domunsncan  9075  domsdomtr  9110  domen1  9117  mapdom1  9140  mapdom2  9146  mapdom3  9147  hartogslem1  9514  harcard  10016  infxpenlem  10049  infpwfien  10098  alephsucdom  10115  mappwen  10148  dfac12lem2  10180  djulepw  10228  fictb  10279  cfflb  10294  canthp1lem1  10694  pwfseqlem5  10705  pwxpndom2  10707  pwdjundom  10709  gchxpidm  10711  gchhar  10721  tskinf  10811  inar1  10817  gruina  10860  rexpen  16349  mreexdomd  17770  lindsdom  22103  hauspwdom  23767  rectbntr0  25099  rabfodom  33020  snct  33224  dya2iocct  34832  karddom  35748  finminlem  37022  iccioo01  38164  pibt2  38254  poimirlem26  38478  heiborlem3  38661  pellexlem4  43771  pellexlem5  43772  safesnsupfidom1o  44355  sn1dom  44464  mpct  46130  thincciso2  50479  aacllem  50855