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

Theorem endom 7606
Description: Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
Assertion
Ref Expression
endom  |-  ( A 
~~  B  ->  A  ~<_  B )

Proof of Theorem endom
StepHypRef Expression
1 enssdom 7604 . 2  |-  ~~  C_  ~<_
21ssbri 4466 1  |-  ( A 
~~  B  ->  A  ~<_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   class class class wbr 4423    ~~ cen 7577    ~<_ cdom 7578
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-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
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 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-xp 4859  df-rel 4860  df-f1o 5608  df-en 7581  df-dom 7582
This theorem is referenced by:  bren2  7610  domrefg  7614  endomtr  7637  domentr  7638  domunsncan  7681  sbthb  7702  sdomentr  7715  ensdomtr  7717  domtriord  7727  domunsn  7731  xpen  7744  unxpdom2  7789  sucxpdom  7790  wdomen1  8100  wdomen2  8101  fidomtri2  8436  prdom2  8445  acnen  8491  acnen2  8493  alephdom  8519  alephinit  8533  uncdadom  8608  pwcdadom  8653  fin1a2lem11  8847  hsmexlem1  8863  gchdomtri  9061  gchcdaidm  9100  gchxpidm  9101  gchpwdom  9102  gchhar  9111  gruina  9250  odinf  17213  hauspwdom  20514  ufildom1  20939  iscmet3  22261  ovolctb2  22443  mbfaddlem  22614  nnct  28296  heiborlem3  32109  zct  37374  caratheodory  38257
  Copyright terms: Public domain W3C validator