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

Theorem ssdomg 7112
Description: A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
ssdomg  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )

Proof of Theorem ssdomg
StepHypRef Expression
1 ssexg 4309 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
2 simpr 448 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  B  e.  V )
3 f1oi 5672 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5639 . . . . . . . . . 10  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A )
) )
53, 4mpbi 200 . . . . . . . . 9  |-  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A ) )
65simpli 445 . . . . . . . 8  |-  (  _I  |`  A ) : A -onto-> A
7 fof 5612 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 8 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5558 . . . . . . 7  |-  ( ( (  _I  |`  A ) : A --> A  /\  A  C_  B )  -> 
(  _I  |`  A ) : A --> B )
108, 9mpan 652 . . . . . 6  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A --> B )
11 funi 5442 . . . . . . . 8  |-  Fun  _I
12 cnvi 5235 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5433 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 201 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5480 . . . . . . 7  |-  ( Fun  `'  _I  ->  Fun  `' (  _I  |`  A )
)
1614, 15ax-mp 8 . . . . . 6  |-  Fun  `' (  _I  |`  A )
1710, 16jctir 525 . . . . 5  |-  ( A 
C_  B  ->  (
(  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A ) ) )
18 df-f1 5418 . . . . 5  |-  ( (  _I  |`  A ) : A -1-1-> B  <->  ( (  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A )
) )
1917, 18sylibr 204 . . . 4  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A -1-1-> B )
2019adantr 452 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  (  _I  |`  A ) : A -1-1-> B )
21 f1dom2g 7084 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1184 . 2  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  ~<_  B )
2322expcom 425 1  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   _Vcvv 2916    C_ wss 3280   class class class wbr 4172    _I cid 4453   `'ccnv 4836    |` cres 4839   Fun wfun 5407   -->wf 5409   -1-1->wf1 5410   -onto->wfo 5411   -1-1-onto->wf1o 5412    ~<_ cdom 7066
This theorem is referenced by:  undom  7155  xpdom3  7165  domunsncan  7167  0domg  7193  domtriord  7212  sdomel  7213  sdomdif  7214  onsdominel  7215  pwdom  7218  2pwuninel  7221  mapdom1  7231  mapdom3  7238  limenpsi  7241  php  7250  php2  7251  php3  7252  onomeneq  7255  nndomo  7259  sucdom2  7262  unbnn  7322  nnsdomg  7325  fodomfi  7344  fidomdm  7347  pwfilem  7359  hartogslem1  7467  hartogs  7469  card2on  7478  wdompwdom  7502  wdom2d  7504  wdomima2g  7510  unxpwdom2  7512  unxpwdom  7513  harwdom  7514  r1sdom  7656  tskwe  7793  carddomi2  7813  cardsdomelir  7816  cardsdomel  7817  harcard  7821  carduni  7824  cardmin2  7841  infxpenlem  7851  ssnum  7876  acnnum  7889  fodomfi2  7897  inffien  7900  alephordi  7911  dfac12lem2  7980  cdadom3  8024  cdainflem  8027  cdainf  8028  unctb  8041  infunabs  8043  infcda  8044  infdif  8045  infdif2  8046  infmap2  8054  ackbij2  8079  fictb  8081  cfslb  8102  fincssdom  8159  fin67  8231  fin1a2lem12  8247  axcclem  8293  brdom3  8362  brdom5  8363  brdom4  8364  imadomg  8368  ondomon  8394  alephval2  8403  alephadd  8408  alephmul  8409  alephexp1  8410  alephsuc3  8411  alephexp2  8412  alephreg  8413  pwcfsdom  8414  cfpwsdom  8415  canthnum  8480  pwfseqlem5  8494  pwxpndom2  8496  pwcdandom  8498  gchac  8504  gchaleph  8506  gchaleph2  8507  winainflem  8524  gchina  8530  tsksdom  8587  tskinf  8600  inttsk  8605  inar1  8606  inatsk  8609  tskord  8611  tskcard  8612  grudomon  8648  gruina  8649  axgroth2  8656  axgroth6  8659  grothac  8661  hashun2  11612  hashsslei  11640  isercoll  12416  o1fsum  12547  incexc2  12573  xpnnenOLD  12764  znnen  12767  qnnen  12768  rpnnen  12781  ruc  12797  phicl2  13112  phibnd  13115  4sqlem11  13278  vdwlem11  13314  0ram  13343  mreexdomd  13829  pgpssslw  15203  fislw  15214  cctop  17025  1stcfb  17461  2ndc1stc  17467  1stcrestlem  17468  2ndcctbss  17471  2ndcdisj2  17473  2ndcsep  17475  dis2ndc  17476  csdfil  17879  ufilen  17915  opnreen  18815  rectbntr0  18816  ovolctb2  19341  uniiccdif  19423  dyadmbl  19445  opnmblALT  19448  vitali  19458  mbfimaopnlem  19500  mbfsup  19509  fta1blem  20044  aannenlem3  20200  ppiwordi  20898  musum  20929  ppiub  20941  chpub  20957  dchrisum0re  21160  dirith2  21175  umgraex  21311  konigsberg  21662  abrexdomjm  23941  ssct  24054  fnct  24058  dmct  24059  cnvct  24060  mptct  24062  mptctf  24065  esumcst  24408  sibfof  24607  subfaclefac  24815  erdszelem10  24839  snmlff  24969  mblfinlem  26143  finminlem  26211  abrexdom  26322  heiborlem3  26412  ctbnfien  26769  pellexlem4  26785  pellexlem5  26786  ttac  26997  idomodle  27380  idomsubgmo  27382
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-dom 7070
  Copyright terms: Public domain W3C validator