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

Theorem ssdomg 7120
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 4317 . . 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 5680 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5647 . . . . . . . . . 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 5620 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 8 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5566 . . . . . . 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 5450 . . . . . . . 8  |-  Fun  _I
12 cnvi 5243 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5441 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 201 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5488 . . . . . . 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 5426 . . . . 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 7092 . . 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 2924    C_ wss 3288   class class class wbr 4180    _I cid 4461   `'ccnv 4844    |` cres 4847   Fun wfun 5415   -->wf 5417   -1-1->wf1 5418   -onto->wfo 5419   -1-1-onto->wf1o 5420    ~<_ cdom 7074
This theorem is referenced by:  undom  7163  xpdom3  7173  domunsncan  7175  0domg  7201  domtriord  7220  sdomel  7221  sdomdif  7222  onsdominel  7223  pwdom  7226  2pwuninel  7229  mapdom1  7239  mapdom3  7246  limenpsi  7249  php  7258  php2  7259  php3  7260  onomeneq  7263  nndomo  7267  sucdom2  7270  unbnn  7330  nnsdomg  7333  fodomfi  7352  fidomdm  7355  pwfilem  7367  hartogslem1  7475  hartogs  7477  card2on  7486  wdompwdom  7510  wdom2d  7512  wdomima2g  7518  unxpwdom2  7520  unxpwdom  7521  harwdom  7522  r1sdom  7664  tskwe  7801  carddomi2  7821  cardsdomelir  7824  cardsdomel  7825  harcard  7829  carduni  7832  cardmin2  7849  infxpenlem  7859  ssnum  7884  acnnum  7897  fodomfi2  7905  inffien  7908  alephordi  7919  dfac12lem2  7988  cdadom3  8032  cdainflem  8035  cdainf  8036  unctb  8049  infunabs  8051  infcda  8052  infdif  8053  infdif2  8054  infmap2  8062  ackbij2  8087  fictb  8089  cfslb  8110  fincssdom  8167  fin67  8239  fin1a2lem12  8255  axcclem  8301  brdom3  8370  brdom5  8371  brdom4  8372  imadomg  8376  ondomon  8402  alephval2  8411  alephadd  8416  alephmul  8417  alephexp1  8418  alephsuc3  8419  alephexp2  8420  alephreg  8421  pwcfsdom  8422  cfpwsdom  8423  canthnum  8488  pwfseqlem5  8502  pwxpndom2  8504  pwcdandom  8506  gchac  8512  gchaleph  8514  gchaleph2  8515  winainflem  8532  gchina  8538  tsksdom  8595  tskinf  8608  inttsk  8613  inar1  8614  inatsk  8617  tskord  8619  tskcard  8620  grudomon  8656  gruina  8657  axgroth2  8664  axgroth6  8667  grothac  8669  hashun2  11620  hashsslei  11648  isercoll  12424  o1fsum  12555  incexc2  12581  xpnnenOLD  12772  znnen  12775  qnnen  12776  rpnnen  12789  ruc  12805  phicl2  13120  phibnd  13123  4sqlem11  13286  vdwlem11  13322  0ram  13351  mreexdomd  13837  pgpssslw  15211  fislw  15222  cctop  17033  1stcfb  17469  2ndc1stc  17475  1stcrestlem  17476  2ndcctbss  17479  2ndcdisj2  17481  2ndcsep  17483  dis2ndc  17484  csdfil  17887  ufilen  17923  opnreen  18823  rectbntr0  18824  ovolctb2  19349  uniiccdif  19431  dyadmbl  19453  opnmblALT  19456  vitali  19466  mbfimaopnlem  19508  mbfsup  19517  fta1blem  20052  aannenlem3  20208  ppiwordi  20906  musum  20937  ppiub  20949  chpub  20965  dchrisum0re  21168  dirith2  21183  umgraex  21319  konigsberg  21670  abrexdomjm  23949  ssct  24062  fnct  24066  dmct  24067  cnvct  24068  mptct  24070  mptctf  24073  esumcst  24416  sibfof  24615  subfaclefac  24823  erdszelem10  24847  snmlff  24977  mblfinlem  26151  finminlem  26219  abrexdom  26330  heiborlem3  26420  ctbnfien  26777  pellexlem4  26793  pellexlem5  26794  ttac  27005  idomodle  27388  idomsubgmo  27390
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 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
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 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-dom 7078
  Copyright terms: Public domain W3C validator