MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ensdomtr Structured version   Visualization version   GIF version

Theorem ensdomtr 8650
Description: Transitivity of equinumerosity and strict dominance. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
ensdomtr ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)

Proof of Theorem ensdomtr
StepHypRef Expression
1 endom 8532 . 2 (𝐴𝐵𝐴𝐵)
2 domsdomtr 8649 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
31, 2sylan 583 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   class class class wbr 5052  cen 8502  cdom 8503  csdm 8504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-er 8285  df-en 8506  df-dom 8507  df-sdom 8508
This theorem is referenced by:  sdomen1  8658  sucxpdom  8724  f1finf1o  8742  findcard3  8758  isfinite2  8773  pm54.43  9427  infxpenlem  9437  alephnbtwn2  9496  alephordi  9498  alephsucdom  9503  pwsdompw  9624  infunsdom1  9633  cflim2  9683  fin23lem27  9748  cfpwsdom  10004  inawinalem  10109  inar1  10195  tskcard  10201  tskuni  10203  rpnnen  15580  resdomq  15597  aleph1re  15598  aleph1irr  15599  1nprm  16021  ensucne0OLD  40159
  Copyright terms: Public domain W3C validator