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

Theorem suppss2 6726
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 2443 . . . . 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 6714 . . . 4  |-  ( ( Z  e.  _V  /\  ph )  ->  ( (
k  e.  A  |->  B ) supp  Z )  =  { k  e.  A  |  B  e.  ( _V  \  { Z }
) } )
6 eldifsni 4004 . . . . . . 7  |-  ( B  e.  ( _V  \  { Z } )  ->  B  =/=  Z )
7 eldif 3341 . . . . . . . . . 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 2681 . . . . . . 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 3435 . . . 4  |-  ( ( Z  e.  _V  /\  ph )  ->  { k  e.  A  |  B  e.  ( _V  \  { Z } ) }  C_  W )
165, 15eqsstrd 3393 . . 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 6696 . . . . 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 3669 . . . 4  |-  (/)  C_  W
2321, 22syl6eqss 3409 . . 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 2609   {crab 2722   _Vcvv 2975    \ cdif 3328    C_ wss 3331   (/)c0 3640   {csn 3880    e. cmpt 4353  (class class class)co 6094   supp csupp 6693
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 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375
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 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-reu 2725  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-iun 4176  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-supp 6694
This theorem is referenced by:  suppsssn  6727  fsuppmptif  7652  sniffsupp  7662  cantnflem1d  7899  cantnflem1  7900  gsumzsplit  16421  gsummpt1n0  16459  gsum2dlem1  16464  gsum2dlem2  16465  gsum2d  16466  dprdfid  16510  dprdfinv  16512  dprdfadd  16513  dmdprdsplitlem  16537  dpjidcl  16560  psrbagaddcl  17441  psrlidm  17477  psrridm  17479  mplsubrg  17522  mplmon  17545  mplmonmul  17546  mplcoe1  17547  mplcoe5  17551  mplbas2  17554  evlslem4  17594  evlslem2  17600  evlslem3  17603  evlslem1  17604  coe1tmmul2  17732  coe1tmmul  17733  uvcff  18219  uvcresum  18221  tsmssplit  19729  coe1mul3  21574  plypf1  21683  tayl0  21830  suppss3  26030
  Copyright terms: Public domain W3C validator