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

Theorem domentr 8562
Description: Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
Assertion
Ref Expression
domentr ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)

Proof of Theorem domentr
StepHypRef Expression
1 endom 8530 . 2 (𝐵𝐶𝐵𝐶)
2 domtr 8556 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
31, 2sylan2 592 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   class class class wbr 5063  cen 8500  cdom 8501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-f1o 6361  df-en 8504  df-dom 8505
This theorem is referenced by:  domdifsn  8594  xpdom1g  8608  domunsncan  8611  sdomdomtr  8644  domen2  8654  mapdom2  8682  php  8695  unxpdom2  8720  sucxpdom  8721  xpfir  8734  fodomfi  8791  cardsdomelir  9396  infxpenlem  9433  xpct  9436  infpwfien  9482  inffien  9483  mappwen  9532  iunfictbso  9534  djuxpdom  9605  cdainflem  9607  djuinf  9608  djulepw  9612  ficardun2  9619  unctb  9621  infdjuabs  9622  infunabs  9623  infdju  9624  infdif  9625  infxpdom  9627  pwdjudom  9632  infmap2  9634  fictb  9661  cfslb  9682  fin1a2lem11  9826  fnct  9953  unirnfdomd  9983  iunctb  9990  alephreg  9998  cfpwsdom  10000  gchdomtri  10045  canthp1lem1  10068  pwfseqlem5  10079  pwxpndom  10082  gchdjuidm  10084  gchxpidm  10085  gchpwdom  10086  gchhar  10095  inttsk  10190  inar1  10191  tskcard  10197  znnen  15560  qnnen  15561  rpnnen  15575  rexpen  15576  aleph1irr  15594  cygctb  18948  1stcfb  21988  2ndcredom  21993  2ndcctbss  21998  hauspwdom  22044  tx2ndc  22194  met1stc  23065  met2ndci  23066  re2ndc  23343  opnreen  23373  ovolctb2  24027  ovolfi  24029  uniiccdif  24113  dyadmbl  24135  opnmblALT  24138  vitali  24148  mbfimaopnlem  24190  mbfsup  24199  aannenlem3  24853  dmvlsiga  31293  sigapildsys  31326  omssubadd  31463  carsgclctunlem3  31483  finminlem  33569  phpreu  34762  lindsdom  34772  mblfinlem1  34815  pellexlem4  39313  pellexlem5  39314  pr2dom  39777  tr3dom  39778  nnfoctb  41193  ioonct  41697  subsaliuncl  42526  caragenunicl  42691  aacllem  44804
  Copyright terms: Public domain W3C validator