Theorem endomtr 9021

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   class class class wbr 5107   ≈ cen 8952   ≼ cdom 8953

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 2215  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-pr 5402  ax-un 7739

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-f1o 6544  df-en 8956  df-dom 8957

This theorem is used by:  cnvct  9044  xpdom1g  9075  xpdom3  9076  domunsncan  9078  domsdomtr  9113  domen1  9120  mapdom1  9143  mapdom2  9149  mapdom3  9150  hartogslem1  9517  harcard  9986  infxpenlem  10019  infpwfien  10068  alephsucdom  10085  mappwen  10118  dfac12lem2  10150  djulepw  10198  fictb  10249  cfflb  10264  canthp1lem1  10664  pwfseqlem5  10675  pwxpndom2  10677  pwdjundom  10679  gchxpidm  10681  gchhar  10691  tskinf  10781  inar1  10787  gruina  10830  rexpen  16320  mreexdomd  17741  lindsdom  22064  hauspwdom  23728  rectbntr0  25060  rabfodom  32966  snct  33171  dya2iocct  34778  karddom  35674  finminlem  36924  iccioo01  38068  pibt2  38158  poimirlem26  38382  heiborlem3  38550  pellexlem4  43660  pellexlem5  43661  safesnsupfidom1o  44244  sn1dom  44353  mpct  46019  thincciso2  50368  aacllem  50759