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

Theorem domentr 7574
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 7542 . 2  |-  ( B 
~~  C  ->  B  ~<_  C )
2 domtr 7568 . 2  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
31, 2sylan2 474 1  |-  ( ( A  ~<_  B  /\  B  ~~  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   class class class wbr 4447    ~~ cen 7513    ~<_ cdom 7514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-f1o 5595  df-en 7517  df-dom 7518
This theorem is referenced by:  domdifsn  7600  xpdom1g  7614  domunsncan  7617  sdomdomtr  7650  domen2  7660  mapdom2  7688  php  7701  unxpdom2  7728  sucxpdom  7729  xpfir  7742  fodomfi  7799  cardsdomelir  8354  infxpenlem  8391  infpwfien  8443  inffien  8444  mappwen  8493  iunfictbso  8495  cdaxpdom  8569  cdainflem  8571  cdainf  8572  cdalepw  8576  ficardun2  8583  unctb  8585  infcdaabs  8586  infunabs  8587  infcda  8588  infdif  8589  infxpdom  8591  pwcdadom  8596  infmap2  8598  fictb  8625  cfslb  8646  fin1a2lem11  8790  unirnfdomd  8942  iunctb  8949  alephreg  8957  cfpwsdom  8959  gchdomtri  9007  canthp1lem1  9030  pwfseqlem5  9041  pwxpndom  9044  gchcdaidm  9046  gchxpidm  9047  gchpwdom  9048  gchhar  9057  inttsk  9152  inar1  9153  tskcard  9159  znnen  13807  qnnen  13808  rpnnen  13821  rexpen  13822  aleph1irr  13840  cygctb  16697  1stcfb  19740  2ndcredom  19745  2ndcctbss  19750  hauspwdom  19796  tx1stc  19914  tx2ndc  19915  met1stc  20787  met2ndci  20788  re2ndc  21069  opnreen  21099  ovolctb2  21666  ovolfi  21668  uniiccdif  21750  dyadmbl  21772  opnmblALT  21775  vitali  21785  mbfimaopnlem  21825  mbfsup  21834  aannenlem3  22488  xpct  27233  fnct  27236  dmvlsiga  27797  mblfinlem1  29656  finminlem  29741  pellexlem4  30400  pellexlem5  30401
  Copyright terms: Public domain W3C validator