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

Theorem ssdomg 6907
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 4160 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
2 simpr 447 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  B  e.  V )
3 f1oi 5511 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5478 . . . . . . . . . 10  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A )
) )
53, 4mpbi 199 . . . . . . . . 9  |-  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A ) )
65simpli 444 . . . . . . . 8  |-  (  _I  |`  A ) : A -onto-> A
7 fof 5451 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 8 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5397 . . . . . . 7  |-  ( ( (  _I  |`  A ) : A --> A  /\  A  C_  B )  -> 
(  _I  |`  A ) : A --> B )
108, 9mpan 651 . . . . . 6  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A --> B )
11 funi 5284 . . . . . . . 8  |-  Fun  _I
12 cnvi 5085 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5275 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 200 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5320 . . . . . . 7  |-  ( Fun  `'  _I  ->  Fun  `' (  _I  |`  A )
)
1614, 15ax-mp 8 . . . . . 6  |-  Fun  `' (  _I  |`  A )
1710, 16jctir 524 . . . . 5  |-  ( A 
C_  B  ->  (
(  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A ) ) )
18 df-f1 5260 . . . . 5  |-  ( (  _I  |`  A ) : A -1-1-> B  <->  ( (  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A )
) )
1917, 18sylibr 203 . . . 4  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A -1-1-> B )
2019adantr 451 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  (  _I  |`  A ) : A -1-1-> B )
21 f1dom2g 6879 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1182 . 2  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  ~<_  B )
2322expcom 424 1  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   _Vcvv 2788    C_ wss 3152   class class class wbr 4023    _I cid 4304   `'ccnv 4688    |` cres 4691   Fun wfun 5249   -->wf 5251   -1-1->wf1 5252   -onto->wfo 5253   -1-1-onto->wf1o 5254    ~<_ cdom 6861
This theorem is referenced by:  undom  6950  xpdom3  6960  domunsncan  6962  0domg  6988  domtriord  7007  sdomel  7008  sdomdif  7009  onsdominel  7010  pwdom  7013  2pwuninel  7016  mapdom1  7026  mapdom3  7033  limenpsi  7036  php  7045  php2  7046  php3  7047  onomeneq  7050  nndomo  7054  sucdom2  7057  unbnn  7113  nnsdomg  7116  fodomfi  7135  fidomdm  7138  pwfilem  7150  hartogslem1  7257  hartogs  7259  card2on  7268  wdompwdom  7292  wdom2d  7294  wdomima2g  7300  unxpwdom2  7302  unxpwdom  7303  harwdom  7304  r1sdom  7446  tskwe  7583  carddomi2  7603  cardsdomelir  7606  cardsdomel  7607  harcard  7611  carduni  7614  cardmin2  7631  infxpenlem  7641  ssnum  7666  acnnum  7679  fodomfi2  7687  inffien  7690  alephordi  7701  dfac12lem2  7770  cdadom3  7814  cdainflem  7817  cdainf  7818  unctb  7831  infunabs  7833  infcda  7834  infdif  7835  infdif2  7836  infmap2  7844  ackbij2  7869  fictb  7871  cfslb  7892  fincssdom  7949  fin67  8021  fin1a2lem12  8037  axcclem  8083  brdom3  8153  brdom5  8154  brdom4  8155  imadomg  8159  ondomon  8185  alephval2  8194  alephadd  8199  alephmul  8200  alephexp1  8201  alephsuc3  8202  alephexp2  8203  alephreg  8204  pwcfsdom  8205  cfpwsdom  8206  canthnum  8271  pwfseqlem5  8285  pwxpndom2  8287  pwcdandom  8289  gchac  8295  gchaleph  8297  gchaleph2  8298  winainflem  8315  gchina  8321  tsksdom  8378  tskinf  8391  inttsk  8396  inar1  8397  inatsk  8400  tskord  8402  tskcard  8403  grudomon  8439  gruina  8440  axgroth2  8447  axgroth6  8450  grothac  8452  hashun2  11365  hashsslei  11378  isercoll  12141  o1fsum  12271  incexc2  12297  xpnnenOLD  12488  znnen  12491  qnnen  12492  rpnnen  12505  ruc  12521  phicl2  12836  phibnd  12839  4sqlem11  13002  vdwlem11  13038  0ram  13067  mreexdomd  13551  pgpssslw  14925  fislw  14936  cctop  16743  1stcfb  17171  2ndc1stc  17177  1stcrestlem  17178  2ndcctbss  17181  2ndcdisj2  17183  2ndcsep  17185  dis2ndc  17186  csdfil  17589  ufilen  17625  opnreen  18336  rectbntr0  18337  ovolctb2  18851  uniiccdif  18933  dyadmbl  18955  opnmblALT  18958  vitali  18968  mbfimaopnlem  19010  mbfsup  19019  fta1blem  19554  aannenlem3  19710  ppiwordi  20400  musum  20431  ppiub  20443  chpub  20459  dchrisum0re  20662  dirith2  20677  abrexdomjm  23165  ssct  23337  fnct  23341  dmct  23342  cnvct  23343  mptct  23345  mptctf  23348  esumcst  23436  subfaclefac  23707  erdszelem10  23731  umgraex  23875  konigsberg  23911  snmlff  23912  sndw  25100  carinttar  25902  finminlem  26231  abrexdom  26405  heiborlem3  26537  ctbnfien  26901  pellexlem4  26917  pellexlem5  26918  ttac  27129  idomodle  27512  idomsubgmo  27514
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-dom 6865
  Copyright terms: Public domain W3C validator