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

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

Proof of Theorem endomtr
StepHypRef Expression
1 endom 7535 . 2  |-  ( A 
~~  B  ->  A  ~<_  B )
2 domtr 7561 . 2  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
31, 2sylan 469 1  |-  ( ( A  ~~  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   class class class wbr 4439    ~~ cen 7506    ~<_ cdom 7507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-f1o 5577  df-en 7510  df-dom 7511
This theorem is referenced by:  undom  7598  xpdom1g  7607  xpdom3  7608  domunsncan  7610  domsdomtr  7645  domen1  7652  mapdom1  7675  mapdom2  7681  mapdom3  7682  php  7694  onomeneq  7700  sucdom2  7707  hartogslem1  7959  harcard  8350  infxpenlem  8382  infpwfien  8434  alephsucdom  8451  mappwen  8484  dfac12lem2  8515  cdalepw  8567  fictb  8616  cfflb  8630  canthp1lem1  9019  pwfseqlem5  9030  pwxpndom2  9032  pwcdandom  9034  gchxpidm  9036  gchhar  9046  tskinf  9136  inar1  9142  gruina  9185  xpnnenOLD  14030  rexpen  14048  mreexdomd  15141  hauspwdom  20171  rectbntr0  21506  rabfodom  27606  snct  27767  cnvct  27771  dya2iocct  28491  finminlem  30379  heiborlem3  30552  pellexlem4  31010  pellexlem5  31011  aacllem  33623
  Copyright terms: Public domain W3C validator