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

Theorem endomtr 7581
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 7550 . 2  |-  ( A 
~~  B  ->  A  ~<_  B )
2 domtr 7576 . 2  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
31, 2sylan 473 1  |-  ( ( A  ~~  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   class class class wbr 4366    ~~ cen 7521    ~<_ cdom 7522
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 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541
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 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-f1o 5551  df-en 7525  df-dom 7526
This theorem is referenced by:  undom  7613  xpdom1g  7622  xpdom3  7623  domunsncan  7625  domsdomtr  7660  domen1  7667  mapdom1  7690  mapdom2  7696  mapdom3  7697  php  7709  onomeneq  7715  sucdom2  7721  hartogslem1  8010  harcard  8364  infxpenlem  8396  infpwfien  8444  alephsucdom  8461  mappwen  8494  dfac12lem2  8525  cdalepw  8577  fictb  8626  cfflb  8640  canthp1lem1  9028  pwfseqlem5  9039  pwxpndom2  9041  pwcdandom  9043  gchxpidm  9045  gchhar  9055  tskinf  9145  inar1  9151  gruina  9194  rexpen  14223  mreexdomd  15498  hauspwdom  20458  rectbntr0  21792  rabfodom  28083  snct  28245  cnvct  28249  dya2iocct  29054  finminlem  30923  poimirlem26  31873  heiborlem3  32052  pellexlem4  35589  pellexlem5  35590  aacllem  40143
  Copyright terms: Public domain W3C validator