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

Theorem domentr 7593
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 7561 . 2  |-  ( B 
~~  C  ->  B  ~<_  C )
2 domtr 7587 . 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 4456    ~~ cen 7532    ~<_ cdom 7533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-f1o 5601  df-en 7536  df-dom 7537
This theorem is referenced by:  domdifsn  7619  xpdom1g  7633  domunsncan  7636  sdomdomtr  7669  domen2  7679  mapdom2  7707  php  7720  unxpdom2  7747  sucxpdom  7748  xpfir  7761  fodomfi  7817  cardsdomelir  8371  infxpenlem  8408  infpwfien  8460  inffien  8461  mappwen  8510  iunfictbso  8512  cdaxpdom  8586  cdainflem  8588  cdainf  8589  cdalepw  8593  ficardun2  8600  unctb  8602  infcdaabs  8603  infunabs  8604  infcda  8605  infdif  8606  infxpdom  8608  pwcdadom  8613  infmap2  8615  fictb  8642  cfslb  8663  fin1a2lem11  8807  unirnfdomd  8959  iunctb  8966  alephreg  8974  cfpwsdom  8976  gchdomtri  9024  canthp1lem1  9047  pwfseqlem5  9058  pwxpndom  9061  gchcdaidm  9063  gchxpidm  9064  gchpwdom  9065  gchhar  9074  inttsk  9169  inar1  9170  tskcard  9176  znnen  13958  qnnen  13959  rpnnen  13972  rexpen  13973  aleph1irr  13991  cygctb  17021  1stcfb  20072  2ndcredom  20077  2ndcctbss  20082  hauspwdom  20128  tx1stc  20277  tx2ndc  20278  met1stc  21150  met2ndci  21151  re2ndc  21432  opnreen  21462  ovolctb2  22029  ovolfi  22031  uniiccdif  22113  dyadmbl  22135  opnmblALT  22138  vitali  22148  mbfimaopnlem  22188  mbfsup  22197  aannenlem3  22852  xpct  27690  fnct  27693  dmvlsiga  28302  omssubadd  28444  carsgclctunlem3  28462  mblfinlem1  30235  finminlem  30320  pellexlem4  30951  pellexlem5  30952  aacllem  33339
  Copyright terms: Public domain W3C validator