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

Theorem suppss2 6718
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.) (Revised by AV, 28-May-2019.)
Hypotheses
Ref Expression
suppss2.n  |-  ( (
ph  /\  k  e.  ( A  \  W ) )  ->  B  =  Z )
suppss2.a  |-  ( ph  ->  A  e.  V )
Assertion
Ref Expression
suppss2  |-  ( ph  ->  ( ( k  e.  A  |->  B ) supp  Z
)  C_  W )
Distinct variable groups:    A, k    ph, k    k, W    k, Z
Allowed substitution hints:    B( k)    V( k)

Proof of Theorem suppss2
StepHypRef Expression
1 eqid 2437 . . . . 5  |-  ( k  e.  A  |->  B )  =  ( k  e.  A  |->  B )
2 suppss2.a . . . . . 6  |-  ( ph  ->  A  e.  V )
32adantl 466 . . . . 5  |-  ( ( Z  e.  _V  /\  ph )  ->  A  e.  V )
4 simpl 457 . . . . 5  |-  ( ( Z  e.  _V  /\  ph )  ->  Z  e.  _V )
51, 3, 4mptsuppdifd 6706 . . . 4  |-  ( ( Z  e.  _V  /\  ph )  ->  ( (
k  e.  A  |->  B ) supp  Z )  =  { k  e.  A  |  B  e.  ( _V  \  { Z }
) } )
6 eldifsni 3994 . . . . . . 7  |-  ( B  e.  ( _V  \  { Z } )  ->  B  =/=  Z )
7 eldif 3331 . . . . . . . . . 10  |-  ( k  e.  ( A  \  W )  <->  ( k  e.  A  /\  -.  k  e.  W ) )
8 suppss2.n . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( A  \  W ) )  ->  B  =  Z )
98adantll 713 . . . . . . . . . 10  |-  ( ( ( Z  e.  _V  /\ 
ph )  /\  k  e.  ( A  \  W
) )  ->  B  =  Z )
107, 9sylan2br 476 . . . . . . . . 9  |-  ( ( ( Z  e.  _V  /\ 
ph )  /\  (
k  e.  A  /\  -.  k  e.  W
) )  ->  B  =  Z )
1110expr 615 . . . . . . . 8  |-  ( ( ( Z  e.  _V  /\ 
ph )  /\  k  e.  A )  ->  ( -.  k  e.  W  ->  B  =  Z ) )
1211necon1ad 2672 . . . . . . 7  |-  ( ( ( Z  e.  _V  /\ 
ph )  /\  k  e.  A )  ->  ( B  =/=  Z  ->  k  e.  W ) )
136, 12syl5 32 . . . . . 6  |-  ( ( ( Z  e.  _V  /\ 
ph )  /\  k  e.  A )  ->  ( B  e.  ( _V  \  { Z } )  ->  k  e.  W
) )
14133impia 1184 . . . . 5  |-  ( ( ( Z  e.  _V  /\ 
ph )  /\  k  e.  A  /\  B  e.  ( _V  \  { Z } ) )  -> 
k  e.  W )
1514rabssdv 3425 . . . 4  |-  ( ( Z  e.  _V  /\  ph )  ->  { k  e.  A  |  B  e.  ( _V  \  { Z } ) }  C_  W )
165, 15eqsstrd 3383 . . 3  |-  ( ( Z  e.  _V  /\  ph )  ->  ( (
k  e.  A  |->  B ) supp  Z )  C_  W )
1716ex 434 . 2  |-  ( Z  e.  _V  ->  ( ph  ->  ( ( k  e.  A  |->  B ) supp 
Z )  C_  W
) )
18 id 22 . . . . . 6  |-  ( -.  Z  e.  _V  ->  -.  Z  e.  _V )
1918intnand 907 . . . . 5  |-  ( -.  Z  e.  _V  ->  -.  ( ( k  e.  A  |->  B )  e. 
_V  /\  Z  e.  _V ) )
20 supp0prc 6688 . . . . 5  |-  ( -.  ( ( k  e.  A  |->  B )  e. 
_V  /\  Z  e.  _V )  ->  ( ( k  e.  A  |->  B ) supp  Z )  =  (/) )
2119, 20syl 16 . . . 4  |-  ( -.  Z  e.  _V  ->  ( ( k  e.  A  |->  B ) supp  Z )  =  (/) )
22 0ss 3659 . . . 4  |-  (/)  C_  W
2321, 22syl6eqss 3399 . . 3  |-  ( -.  Z  e.  _V  ->  ( ( k  e.  A  |->  B ) supp  Z ) 
C_  W )
2423a1d 25 . 2  |-  ( -.  Z  e.  _V  ->  (
ph  ->  ( ( k  e.  A  |->  B ) supp 
Z )  C_  W
) )
2517, 24pm2.61i 164 1  |-  ( ph  ->  ( ( k  e.  A  |->  B ) supp  Z
)  C_  W )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756    =/= wne 2600   {crab 2713   _Vcvv 2966    \ cdif 3318    C_ wss 3321   (/)c0 3630   {csn 3870    e. cmpt 4343  (class class class)co 6086   supp csupp 6685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-supp 6686
This theorem is referenced by:  suppsssn  6719  fsuppmptif  7641  sniffsupp  7651  cantnflem1d  7888  cantnflem1  7889  gsumzsplit  16407  gsummptif1n0  16443  gsum2dlem1  16447  gsum2dlem2  16448  gsum2d  16449  dprdfid  16493  dprdfinv  16495  dprdfadd  16496  dmdprdsplitlem  16520  dpjidcl  16543  psrbagaddcl  17412  psrlidm  17448  psrridm  17450  mplsubrg  17493  mplmon  17516  mplmonmul  17517  mplcoe1  17518  mplcoe2  17521  mplbas2  17523  evlslem4  17563  evlslem2  17569  evlslem3  17572  evlslem1  17573  coe1tmmul2  17700  coe1tmmul  17701  uvcff  18185  uvcresum  18187  tsmssplit  19695  coe1mul3  21540  plypf1  21649  tayl0  21796  suppss3  25972
  Copyright terms: Public domain W3C validator