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

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

Proof of Theorem domentr
StepHypRef Expression
1 endom 7841 . 2 (𝐵𝐶𝐵𝐶)
2 domtr 7868 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
31, 2sylan2 489 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   class class class wbr 4573  cen 7811  cdom 7812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-f1o 5793  df-en 7815  df-dom 7816
This theorem is referenced by:  domdifsn  7901  xpdom1g  7915  domunsncan  7918  sdomdomtr  7951  domen2  7961  mapdom2  7989  php  8002  unxpdom2  8026  sucxpdom  8027  xpfir  8040  fodomfi  8097  cardsdomelir  8655  infxpenlem  8692  xpct  8695  infpwfien  8741  inffien  8742  mappwen  8791  iunfictbso  8793  cdaxpdom  8867  cdainflem  8869  cdainf  8870  cdalepw  8874  ficardun2  8881  unctb  8883  infcdaabs  8884  infunabs  8885  infcda  8886  infdif  8887  infxpdom  8889  pwcdadom  8894  infmap2  8896  fictb  8923  cfslb  8944  fin1a2lem11  9088  unirnfdomd  9241  iunctb  9248  alephreg  9256  cfpwsdom  9258  gchdomtri  9303  canthp1lem1  9326  pwfseqlem5  9337  pwxpndom  9340  gchcdaidm  9342  gchxpidm  9343  gchpwdom  9344  gchhar  9353  inttsk  9448  inar1  9449  tskcard  9455  znnen  14722  qnnen  14723  rpnnen  14737  rexpen  14738  aleph1irr  14756  cygctb  18058  1stcfb  20996  2ndcredom  21001  2ndcctbss  21006  hauspwdom  21052  tx1stc  21201  tx2ndc  21202  met1stc  22073  met2ndci  22074  re2ndc  22340  opnreen  22370  ovolctb2  22980  ovolfi  22982  uniiccdif  23065  dyadmbl  23087  opnmblALT  23090  vitali  23101  mbfimaopnlem  23141  mbfsup  23150  aannenlem3  23802  fnct  28678  dmvlsiga  29321  sigapildsys  29354  omssubadd  29491  carsgclctunlem3  29511  finminlem  31284  phpreu  32362  lindsdom  32372  mblfinlem1  32415  pellexlem4  36213  pellexlem5  36214  nnfoctb  38037  ioonct  38411  subsaliuncl  39052  caragenunicl  39214  aacllem  42315
  Copyright terms: Public domain W3C validator