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

Theorem suppss2 6073
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 2283 . . 3  |-  ( k  e.  A  |->  B )  =  ( k  e.  A  |->  B )
21mptpreima 5166 . 2  |-  ( `' ( k  e.  A  |->  B ) " ( _V  \  { Z }
) )  =  {
k  e.  A  |  B  e.  ( _V  \  { Z } ) }
3 eldifsni 3750 . . . . 5  |-  ( B  e.  ( _V  \  { Z } )  ->  B  =/=  Z )
4 eldif 3162 . . . . . . . 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 2513 . . . . 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 3253 . 2  |-  ( ph  ->  { k  e.  A  |  B  e.  ( _V  \  { Z }
) }  C_  W
)
122, 11syl5eqss 3222 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 1623    e. wcel 1684    =/= wne 2446   {crab 2547   _Vcvv 2788    \ cdif 3149    C_ wss 3152   {csn 3640    e. cmpt 4077   `'ccnv 4688   "cima 4692
This theorem is referenced by:  cantnflem1d  7390  cantnflem1  7391  gsumzsplit  15206  gsum2d  15223  dprdfid  15252  dprdfinv  15254  dprdfadd  15255  dmdprdsplitlem  15272  dpjidcl  15293  psrbagaddcl  16116  psrbas  16124  psrlidm  16148  psrridm  16149  mvridlem  16164  mplsubrg  16184  mplmon  16207  mplmonmul  16208  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  mplbas2  16212  evlslem4  16245  evlslem2  16249  coe1tmmul2  16352  coe1tmmul  16353  tsms0  17824  tgptsmscls  17832  tsmssplit  17834  evlslem3  19398  evlslem1  19399  coe1mul3  19485  plypf1  19594  tayl0  19741  dchrptlem3  20505  uvcresum  27242  mamulid  27458  mamurid  27459
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-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
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-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-mpt 4079  df-xp 4695  df-rel 4696  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702
  Copyright terms: Public domain W3C validator