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

Theorem domentr 7635
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 7603 . 2  |-  ( B 
~~  C  ->  B  ~<_  C )
2 domtr 7629 . 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 4426    ~~ cen 7574    ~<_ cdom 7575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-f1o 5608  df-en 7578  df-dom 7579
This theorem is referenced by:  domdifsn  7661  xpdom1g  7675  domunsncan  7678  sdomdomtr  7711  domen2  7721  mapdom2  7749  php  7762  unxpdom2  7786  sucxpdom  7787  xpfir  7800  fodomfi  7856  cardsdomelir  8406  infxpenlem  8443  infpwfien  8491  inffien  8492  mappwen  8541  iunfictbso  8543  cdaxpdom  8617  cdainflem  8619  cdainf  8620  cdalepw  8624  ficardun2  8631  unctb  8633  infcdaabs  8634  infunabs  8635  infcda  8636  infdif  8637  infxpdom  8639  pwcdadom  8644  infmap2  8646  fictb  8673  cfslb  8694  fin1a2lem11  8838  unirnfdomd  8990  iunctb  8997  alephreg  9005  cfpwsdom  9007  gchdomtri  9053  canthp1lem1  9076  pwfseqlem5  9087  pwxpndom  9090  gchcdaidm  9092  gchxpidm  9093  gchpwdom  9094  gchhar  9103  inttsk  9198  inar1  9199  tskcard  9205  znnen  14243  qnnen  14244  rpnnen  14257  rexpen  14258  aleph1irr  14276  cygctb  17461  1stcfb  20391  2ndcredom  20396  2ndcctbss  20401  hauspwdom  20447  tx1stc  20596  tx2ndc  20597  met1stc  21467  met2ndci  21468  re2ndc  21730  opnreen  21760  ovolctb2  22323  ovolfi  22325  uniiccdif  22412  dyadmbl  22435  opnmblALT  22438  vitali  22448  mbfimaopnlem  22488  mbfsup  22497  aannenlem3  23151  xpct  28137  fnct  28140  dmvlsiga  28790  sigapildsys  28823  omssubadd  28961  carsgclctunlem3  28981  finminlem  30759  phpreu  31633  mblfinlem1  31681  pellexlem4  35386  pellexlem5  35387  nnfoctb  37023  caragenunicl  37854  aacllem  39301
  Copyright terms: Public domain W3C validator