Theorem suppssr 6894

Description: A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.)

Hypotheses

Ref	Expression
suppssr.f	|- ( ph -> F : A --> B )
suppssr.n	|- ( ph -> ( F supp Z ) C_ W )
suppssr.a	|- ( ph -> A e. V )
suppssr.z	|- ( ph -> Z e. U )

Assertion

Ref	Expression
suppssr	|- ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )

Proof of Theorem suppssr

Step	Hyp	Ref	Expression
1		eldif 3382	. 2 |- ( X e. ( A \ W ) <-> ( X e. A /\ -. X e. W ) )
2		fvex 5828	. . . . . 6 |- ( F ` X ) e. _V
3		eldifsn 4061	. . . . . 6 |- ( ( F ` X ) e. ( _V \ { Z } ) <-> ( ( F ` X ) e. _V /\ ( F ` X ) =/= Z ) )
4	2, 3	mpbiran 926	. . . . 5 |- ( ( F ` X ) e. ( _V \ { Z } ) <-> ( F ` X ) =/= Z )
5		suppssr.f	. . . . . . . . . 10 |- ( ph -> F : A --> B )
6		ffn 5682	. . . . . . . . . 10 |- ( F : A --> B -> F Fn A )
7	5, 6	syl 17	. . . . . . . . 9 |- ( ph -> F Fn A )
8		suppssr.a	. . . . . . . . 9 |- ( ph -> A e. V )
9		suppssr.z	. . . . . . . . 9 |- ( ph -> Z e. U )
10		elsuppfn 6870	. . . . . . . . 9 |- ( ( F Fn A /\ A e. V /\ Z e. U ) -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
11	7, 8, 9, 10	syl3anc 1264	. . . . . . . 8 |- ( ph -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
12		ibar 506	. . . . . . . . . . 11 |- ( ( F ` X ) e. _V -> ( ( F ` X ) =/= Z <-> ( ( F ` X ) e. _V /\ ( F ` X ) =/= Z ) ) )
13	2, 12	mp1i 13	. . . . . . . . . 10 |- ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z <-> ( ( F ` X ) e. _V /\ ( F ` X ) =/= Z ) ) )
14	13, 3	syl6bbr 266	. . . . . . . . 9 |- ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z <-> ( F ` X ) e. ( _V \ { Z } ) ) )
15	14	pm5.32da 645	. . . . . . . 8 |- ( ph -> ( ( X e. A /\ ( F ` X ) =/= Z ) <-> ( X e. A /\ ( F ` X ) e. ( _V \ { Z } ) ) ) )
16	11, 15	bitrd 256	. . . . . . 7 |- ( ph -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) e. ( _V \ { Z } ) ) ) )
17		suppssr.n	. . . . . . . 8 |- ( ph -> ( F supp Z ) C_ W )
18	17	sseld 3399	. . . . . . 7 |- ( ph -> ( X e. ( F supp Z ) -> X e. W ) )
19	16, 18	sylbird 238	. . . . . 6 |- ( ph -> ( ( X e. A /\ ( F ` X ) e. ( _V \ { Z } ) ) -> X e. W ) )
20	19	expdimp 438	. . . . 5 |- ( ( ph /\ X e. A ) -> ( ( F ` X ) e. ( _V \ { Z } ) -> X e. W ) )
21	4, 20	syl5bir 221	. . . 4 |- ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z -> X e. W ) )
22	21	necon1bd 2613	. . 3 |- ( ( ph /\ X e. A ) -> ( -. X e. W -> ( F ` X ) = Z ) )
23	22	impr 623	. 2 |- ( ( ph /\ ( X e. A /\ -. X e. W ) ) -> ( F ` X ) = Z )
24	1, 23	sylan2b 477	1 |- ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1872   =/= wne 2593   _Vcvv 3016   \ cdif 3369   C_ wss 3372   {csn 3934   Fn wfn 5532   -->wf 5533   ` cfv 5537  (class class class)co 6242   supp csupp 6862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pr 4596  ax-un 6534

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-reu 2715  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3698  df-if 3848  df-sn 3935  df-pr 3937  df-op 3941  df-uni 4156  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-id 4704  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-supp 6863

This theorem is referenced by:  fsuppmptif  7859  fsuppco2  7862  fsuppcor  7863  cantnfp1lem1  8128  cantnfp1lem3  8130  cantnflem1  8139  cnfcom2lem  8151  gsumval3  17477  gsumcllem  17478  gsumzaddlem  17490  gsumzmhm  17506  gsumpt  17530  gsum2dlem1  17538  gsum2dlem2  17539  gsum2d  17540  dprdfinv  17588  dprdfadd  17589  dmdprdsplitlem  17606  dpjidcl  17627  gsumdixp  17773  lcomfsupp  18064  psrbaglesupp  18528  psrbagaddcl  18530  psrbaglefi  18532  mplsubglem  18594  mpllsslem  18595  mplsubrglem  18599  mplmonmul  18624  mplcoe1  18625  mplcoe5  18628  mplbas2  18630  evlslem4  18667  evlslem2  18671  uvcresum  19286  frlmsslsp  19289  rrxcph  22286  rrxmval  22294  rrxmetlem  22296  rrxmet  22297  rrxdstprj1  22298  deg1mul3le  23000  eulerpartlemb  29146