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

Theorem ssdomg 6840
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 4100 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
2 simpr 449 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  B  e.  V )
3 f1oi 5414 . . . . . . . . . 10  |-  (  _I  |`  A ) : A -1-1-onto-> A
4 dff1o3 5381 . . . . . . . . . 10  |-  ( (  _I  |`  A ) : A -1-1-onto-> A  <->  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A )
) )
53, 4mpbi 201 . . . . . . . . 9  |-  ( (  _I  |`  A ) : A -onto-> A  /\  Fun  `' (  _I  |`  A ) )
65simpli 446 . . . . . . . 8  |-  (  _I  |`  A ) : A -onto-> A
7 fof 5354 . . . . . . . 8  |-  ( (  _I  |`  A ) : A -onto-> A  ->  (  _I  |`  A ) : A --> A )
86, 7ax-mp 10 . . . . . . 7  |-  (  _I  |`  A ) : A --> A
9 fss 5300 . . . . . . 7  |-  ( ( (  _I  |`  A ) : A --> A  /\  A  C_  B )  -> 
(  _I  |`  A ) : A --> B )
108, 9mpan 654 . . . . . 6  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A --> B )
11 funi 5188 . . . . . . . 8  |-  Fun  _I
12 cnvi 5038 . . . . . . . . 9  |-  `'  _I  =  _I
1312funeqi 5179 . . . . . . . 8  |-  ( Fun  `'  _I  <->  Fun  _I  )
1411, 13mpbir 202 . . . . . . 7  |-  Fun  `'  _I
15 funres11 5223 . . . . . . 7  |-  ( Fun  `'  _I  ->  Fun  `' (  _I  |`  A )
)
1614, 15ax-mp 10 . . . . . 6  |-  Fun  `' (  _I  |`  A )
1710, 16jctir 526 . . . . 5  |-  ( A 
C_  B  ->  (
(  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A ) ) )
18 df-f1 4651 . . . . 5  |-  ( (  _I  |`  A ) : A -1-1-> B  <->  ( (  _I  |`  A ) : A --> B  /\  Fun  `' (  _I  |`  A )
) )
1917, 18sylibr 205 . . . 4  |-  ( A 
C_  B  ->  (  _I  |`  A ) : A -1-1-> B )
2019adantr 453 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  (  _I  |`  A ) : A -1-1-> B )
21 f1dom2g 6812 . . 3  |-  ( ( A  e.  _V  /\  B  e.  V  /\  (  _I  |`  A ) : A -1-1-> B )  ->  A  ~<_  B )
221, 2, 20, 21syl3anc 1187 . 2  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  ~<_  B )
2322expcom 426 1  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  ~<_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   _Vcvv 2740    C_ wss 3094   class class class wbr 3963    _I cid 4241   `'ccnv 4625    |` cres 4628   Fun wfun 4632   -->wf 4634   -1-1->wf1 4635   -onto->wfo 4636   -1-1-onto->wf1o 4637    ~<_ cdom 6794
This theorem is referenced by:  undom  6883  xpdom3  6893  domunsncan  6895  0domg  6921  domtriord  6940  sdomel  6941  sdomdif  6942  onsdominel  6943  pwdom  6946  2pwuninel  6949  mapdom1  6959  mapdom3  6966  limenpsi  6969  php  6978  php2  6979  php3  6980  onomeneq  6983  nndomo  6987  sucdom2  6990  unbnn  7046  nnsdomg  7049  fodomfi  7068  fidomdm  7071  pwfilem  7083  hartogslem1  7190  hartogs  7192  card2on  7201  wdompwdom  7225  wdom2d  7227  wdomima2g  7233  unxpwdom2  7235  unxpwdom  7236  harwdom  7237  r1sdom  7379  tskwe  7516  carddomi2  7536  cardsdomelir  7539  cardsdomel  7540  harcard  7544  carduni  7547  cardmin2  7564  infxpenlem  7574  ssnum  7599  acnnum  7612  fodomfi2  7620  inffien  7623  alephordi  7634  dfac12lem2  7703  cdadom3  7747  cdainflem  7750  cdainf  7751  unctb  7764  infunabs  7766  infcda  7767  infdif  7768  infdif2  7769  infmap2  7777  ackbij2  7802  fictb  7804  cfslb  7825  fincssdom  7882  fin67  7954  fin1a2lem12  7970  axcclem  8016  brdom3  8086  brdom5  8087  brdom4  8088  imadomg  8092  ondomon  8118  alephval2  8127  alephadd  8132  alephmul  8133  alephexp1  8134  alephsuc3  8135  alephexp2  8136  alephreg  8137  pwcfsdom  8138  cfpwsdom  8139  canthnum  8204  pwfseqlem5  8218  pwxpndom2  8220  pwcdandom  8222  gchac  8228  gchaleph  8230  gchaleph2  8231  winainflem  8248  gchina  8254  tsksdom  8311  tskinf  8324  inttsk  8329  inar1  8330  inatsk  8333  tskord  8335  tskcard  8336  grudomon  8372  gruina  8373  axgroth2  8380  axgroth6  8383  grothac  8385  hashun2  11296  hashsslei  11308  isercoll  12071  o1fsum  12201  xpnnenOLD  12415  znnen  12418  qnnen  12419  rpnnen  12432  ruc  12448  phicl2  12763  phibnd  12766  4sqlem11  12929  vdwlem11  12965  0ram  12994  mreexdomd  13478  pgpssslw  14852  fislw  14863  cctop  16670  1stcfb  17098  2ndc1stc  17104  1stcrestlem  17105  2ndcctbss  17108  2ndcdisj2  17110  2ndcsep  17112  dis2ndc  17113  csdfil  17516  ufilen  17552  opnreen  18263  rectbntr0  18264  ovolctb2  18778  uniiccdif  18860  dyadmbl  18882  opnmblALT  18885  vitali  18895  mbfimaopnlem  18937  mbfsup  18946  fta1blem  19481  aannenlem3  19637  ppiwordi  20327  musum  20358  ppiub  20370  chpub  20386  dchrisum0re  20589  dirith2  20604  subfaclefac  23044  erdszelem10  23068  umgraex  23212  konigsberg  23248  snmlff  23249  sndw  24431  carinttar  25234  finminlem  25563  abrexdom  25737  heiborlem3  25869  ctbnfien  26233  pellexlem4  26249  pellexlem5  26250  ttac  26461  idomodle  26844  idomsubgmo  26846
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pow 4126  ax-pr 4152  ax-un 4449
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-pw 3568  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-id 4246  df-xp 4640  df-rel 4641  df-cnv 4642  df-co 4643  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fun 4648  df-fn 4649  df-f 4650  df-f1 4651  df-fo 4652  df-f1o 4653  df-dom 6798
  Copyright terms: Public domain W3C validator