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

Theorem suppss2 6157
Description: Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 22-Mar-2015.)
Hypothesis
Ref Expression
suppss2.n  |-  ( (
ph  /\  k  e.  ( A  \  W ) )  ->  B  =  Z )
Assertion
Ref Expression
suppss2  |-  ( ph  ->  ( `' ( k  e.  A  |->  B )
" ( _V  \  { Z } ) ) 
C_  W )
Distinct variable groups:    A, k    ph, k    k, W    k, Z
Allowed substitution hint:    B( k)

Proof of Theorem suppss2
StepHypRef Expression
1 eqid 2358 . . 3  |-  ( k  e.  A  |->  B )  =  ( k  e.  A  |->  B )
21mptpreima 5245 . 2  |-  ( `' ( k  e.  A  |->  B ) " ( _V  \  { Z }
) )  =  {
k  e.  A  |  B  e.  ( _V  \  { Z } ) }
3 eldifsni 3826 . . . . 5  |-  ( B  e.  ( _V  \  { Z } )  ->  B  =/=  Z )
4 eldif 3238 . . . . . . . 8  |-  ( k  e.  ( A  \  W )  <->  ( k  e.  A  /\  -.  k  e.  W ) )
5 suppss2.n . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( A  \  W ) )  ->  B  =  Z )
64, 5sylan2br 462 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  A  /\  -.  k  e.  W ) )  ->  B  =  Z )
76expr 598 . . . . . 6  |-  ( (
ph  /\  k  e.  A )  ->  ( -.  k  e.  W  ->  B  =  Z ) )
87necon1ad 2588 . . . . 5  |-  ( (
ph  /\  k  e.  A )  ->  ( B  =/=  Z  ->  k  e.  W ) )
93, 8syl5 28 . . . 4  |-  ( (
ph  /\  k  e.  A )  ->  ( B  e.  ( _V  \  { Z } )  ->  k  e.  W
) )
1093impia 1148 . . 3  |-  ( (
ph  /\  k  e.  A  /\  B  e.  ( _V  \  { Z } ) )  -> 
k  e.  W )
1110rabssdv 3329 . 2  |-  ( ph  ->  { k  e.  A  |  B  e.  ( _V  \  { Z }
) }  C_  W
)
122, 11syl5eqss 3298 1  |-  ( ph  ->  ( `' ( k  e.  A  |->  B )
" ( _V  \  { Z } ) ) 
C_  W )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1642    e. wcel 1710    =/= wne 2521   {crab 2623   _Vcvv 2864    \ cdif 3225    C_ wss 3228   {csn 3716    e. cmpt 4156   `'ccnv 4767   "cima 4771
This theorem is referenced by:  cantnflem1d  7477  cantnflem1  7478  gsumzsplit  15299  gsum2d  15316  dprdfid  15345  dprdfinv  15347  dprdfadd  15348  dmdprdsplitlem  15365  dpjidcl  15386  psrbagaddcl  16209  psrbas  16217  psrlidm  16241  psrridm  16242  mvridlem  16257  mplsubrg  16277  mplmon  16300  mplmonmul  16301  mplcoe1  16302  mplcoe3  16303  mplcoe2  16304  mplbas2  16305  evlslem4  16338  evlslem2  16342  coe1tmmul2  16445  coe1tmmul  16446  tsms0  17920  tgptsmscls  17928  tsmssplit  17930  evlslem3  19496  evlslem1  19497  coe1mul3  19583  plypf1  19692  tayl0  19839  dchrptlem3  20611  uvcresum  26565  mamulid  26781  mamurid  26782
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pr 4293
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4103  df-opab 4157  df-mpt 4158  df-xp 4774  df-rel 4775  df-cnv 4776  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781
  Copyright terms: Public domain W3C validator