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

Theorem domentr 7639
Description: Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
Assertion
Ref Expression
domentr  |-  ( ( A  ~<_  B  /\  B  ~~  C )  ->  A  ~<_  C )

Proof of Theorem domentr
StepHypRef Expression
1 endom 7607 . 2  |-  ( B 
~~  C  ->  B  ~<_  C )
2 domtr 7633 . 2  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
31, 2sylan2 476 1  |-  ( ( A  ~<_  B  /\  B  ~~  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   class class class wbr 4423    ~~ cen 7578    ~<_ cdom 7579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-f1o 5608  df-en 7582  df-dom 7583
This theorem is referenced by:  domdifsn  7665  xpdom1g  7679  domunsncan  7682  sdomdomtr  7715  domen2  7725  mapdom2  7753  php  7766  unxpdom2  7790  sucxpdom  7791  xpfir  7804  fodomfi  7860  cardsdomelir  8416  infxpenlem  8453  infpwfien  8501  inffien  8502  mappwen  8551  iunfictbso  8553  cdaxpdom  8627  cdainflem  8629  cdainf  8630  cdalepw  8634  ficardun2  8641  unctb  8643  infcdaabs  8644  infunabs  8645  infcda  8646  infdif  8647  infxpdom  8649  pwcdadom  8654  infmap2  8656  fictb  8683  cfslb  8704  fin1a2lem11  8848  unirnfdomd  9000  iunctb  9007  alephreg  9015  cfpwsdom  9017  gchdomtri  9062  canthp1lem1  9085  pwfseqlem5  9096  pwxpndom  9099  gchcdaidm  9101  gchxpidm  9102  gchpwdom  9103  gchhar  9112  inttsk  9207  inar1  9208  tskcard  9214  znnen  14265  qnnen  14266  rpnnen  14279  rexpen  14280  aleph1irr  14298  cygctb  17526  1stcfb  20459  2ndcredom  20464  2ndcctbss  20469  hauspwdom  20515  tx1stc  20664  tx2ndc  20665  met1stc  21535  met2ndci  21536  re2ndc  21818  opnreen  21848  ovolctb2  22444  ovolfi  22446  uniiccdif  22534  dyadmbl  22557  opnmblALT  22560  vitali  22570  mbfimaopnlem  22610  mbfsup  22619  aannenlem3  23285  xpct  28301  fnct  28304  dmvlsiga  28960  sigapildsys  28993  omssubadd  29137  omssubaddOLD  29141  carsgclctunlem3  29161  finminlem  30980  phpreu  31894  mblfinlem1  31942  pellexlem4  35647  pellexlem5  35648  nnfoctb  37357  caragenunicl  38254  aacllem  40191
  Copyright terms: Public domain W3C validator