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

Theorem endomtr 7379
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 7348 . 2  |-  ( A 
~~  B  ->  A  ~<_  B )
2 domtr 7374 . 2  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
31, 2sylan 471 1  |-  ( ( A  ~~  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   class class class wbr 4304    ~~ cen 7319    ~<_ cdom 7320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-f1o 5437  df-en 7323  df-dom 7324
This theorem is referenced by:  undom  7411  xpdom1g  7420  xpdom3  7421  domunsncan  7423  domsdomtr  7458  domen1  7465  mapdom1  7488  mapdom2  7494  mapdom3  7495  php  7507  onomeneq  7512  sucdom2  7519  hartogslem1  7768  harcard  8160  infxpenlem  8192  infpwfien  8244  alephsucdom  8261  mappwen  8294  dfac12lem2  8325  cdalepw  8377  fictb  8426  cfflb  8440  canthp1lem1  8831  pwfseqlem5  8842  pwxpndom2  8844  pwcdandom  8846  gchxpidm  8848  gchhar  8858  tskinf  8948  inar1  8954  gruina  8997  xpnnenOLD  13504  rexpen  13522  mreexdomd  14599  hauspwdom  19117  rectbntr0  20421  snct  26023  cnvct  26027  dya2iocct  26707  finminlem  28525  heiborlem3  28724  pellexlem4  29185  pellexlem5  29186
  Copyright terms: Public domain W3C validator