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

Theorem ssdomg 7153
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 4349 . . 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 5713 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5680 . . . . . . . . . 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 5653 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 8 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5599 . . . . . . 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 5483 . . . . . . . 8  |-  Fun  _I
12 cnvi 5276 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5474 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 201 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5521 . . . . . . 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 5459 . . . . 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 7125 . . 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 1725   _Vcvv 2956    C_ wss 3320   class class class wbr 4212    _I cid 4493   `'ccnv 4877    |` cres 4880   Fun wfun 5448   -->wf 5450   -1-1->wf1 5451   -onto->wfo 5452   -1-1-onto->wf1o 5453    ~<_ cdom 7107
This theorem is referenced by:  undom  7196  xpdom3  7206  domunsncan  7208  0domg  7234  domtriord  7253  sdomel  7254  sdomdif  7255  onsdominel  7256  pwdom  7259  2pwuninel  7262  mapdom1  7272  mapdom3  7279  limenpsi  7282  php  7291  php2  7292  php3  7293  onomeneq  7296  nndomo  7300  sucdom2  7303  unbnn  7363  nnsdomg  7366  fodomfi  7385  fidomdm  7388  pwfilem  7401  hartogslem1  7511  hartogs  7513  card2on  7522  wdompwdom  7546  wdom2d  7548  wdomima2g  7554  unxpwdom2  7556  unxpwdom  7557  harwdom  7558  r1sdom  7700  tskwe  7837  carddomi2  7857  cardsdomelir  7860  cardsdomel  7861  harcard  7865  carduni  7868  cardmin2  7885  infxpenlem  7895  ssnum  7920  acnnum  7933  fodomfi2  7941  inffien  7944  alephordi  7955  dfac12lem2  8024  cdadom3  8068  cdainflem  8071  cdainf  8072  unctb  8085  infunabs  8087  infcda  8088  infdif  8089  infdif2  8090  infmap2  8098  ackbij2  8123  fictb  8125  cfslb  8146  fincssdom  8203  fin67  8275  fin1a2lem12  8291  axcclem  8337  brdom3  8406  brdom5  8407  brdom4  8408  imadomg  8412  ondomon  8438  alephval2  8447  alephadd  8452  alephmul  8453  alephexp1  8454  alephsuc3  8455  alephexp2  8456  alephreg  8457  pwcfsdom  8458  cfpwsdom  8459  canthnum  8524  pwfseqlem5  8538  pwxpndom2  8540  pwcdandom  8542  gchac  8548  gchaleph  8550  gchaleph2  8551  winainflem  8568  gchina  8574  tsksdom  8631  tskinf  8644  inttsk  8649  inar1  8650  inatsk  8653  tskord  8655  tskcard  8656  grudomon  8692  gruina  8693  axgroth2  8700  axgroth6  8703  grothac  8705  hashun2  11657  hashsslei  11685  isercoll  12461  o1fsum  12592  incexc2  12618  xpnnenOLD  12809  znnen  12812  qnnen  12813  rpnnen  12826  ruc  12842  phicl2  13157  phibnd  13160  4sqlem11  13323  vdwlem11  13359  0ram  13388  mreexdomd  13874  pgpssslw  15248  fislw  15259  cctop  17070  1stcfb  17508  2ndc1stc  17514  1stcrestlem  17515  2ndcctbss  17518  2ndcdisj2  17520  2ndcsep  17522  dis2ndc  17523  csdfil  17926  ufilen  17962  opnreen  18862  rectbntr0  18863  ovolctb2  19388  uniiccdif  19470  dyadmbl  19492  opnmblALT  19495  vitali  19505  mbfimaopnlem  19547  mbfsup  19556  fta1blem  20091  aannenlem3  20247  ppiwordi  20945  musum  20976  ppiub  20988  chpub  21004  dchrisum0re  21207  dirith2  21222  umgraex  21358  konigsberg  21709  abrexdomjm  23988  ssct  24101  fnct  24105  dmct  24106  cnvct  24107  mptct  24109  mptctf  24112  esumcst  24455  sibfof  24654  subfaclefac  24862  erdszelem10  24886  snmlff  25016  mblfinlem1  26243  finminlem  26321  abrexdom  26432  heiborlem3  26522  ctbnfien  26879  pellexlem4  26895  pellexlem5  26896  ttac  27107  idomodle  27489  idomsubgmo  27491
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-dom 7111
  Copyright terms: Public domain W3C validator