Theorem suppssr

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

	Ref	Expression
Hypotheses	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	suppssr	|- ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )

Proof

Step	Hyp	Ref	Expression
1		suppssr.f	|- ( ph -> F : A --> B )
2		suppssr.n	|- ( ph -> ( F supp Z ) C_ W )
3		suppssr.a	|- ( ph -> A e. V )
4		suppssr.z	|- ( ph -> Z e. U )
5		eldif	|- ( X e. ( A \ W ) <-> ( X e. A /\ -. X e. W ) )
6		fvex	|- ( F ` X ) e. _V
7		eldifsn	|- ( ( F ` X ) e. ( _V \ { Z } ) <-> ( ( F ` X ) e. _V /\ ( F ` X ) =/= Z ) )
8	6 7	mpbiran	|- ( ( F ` X ) e. ( _V \ { Z } ) <-> ( F ` X ) =/= Z )
9	1	ffnd	|- ( ph -> F Fn A )
10		elsuppfn	|- ( ( F Fn A /\ A e. V /\ Z e. U ) -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
11	9 3 4 10	syl3anc	|- ( ph -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
12		ibar	|- ( ( F ` X ) e. _V -> ( ( F ` X ) =/= Z <-> ( ( F ` X ) e. _V /\ ( F ` X ) =/= Z ) ) )
13	6 12	mp1i	|- ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z <-> ( ( F ` X ) e. _V /\ ( F ` X ) =/= Z ) ) )
14	13 7	bitr4di	|- ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z <-> ( F ` X ) e. ( _V \ { Z } ) ) )
15	14	pm5.32da	|- ( ph -> ( ( X e. A /\ ( F ` X ) =/= Z ) <-> ( X e. A /\ ( F ` X ) e. ( _V \ { Z } ) ) ) )
16	11 15	bitrd	|- ( ph -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) e. ( _V \ { Z } ) ) ) )
17	2	sseld	|- ( ph -> ( X e. ( F supp Z ) -> X e. W ) )
18	16 17	sylbird	|- ( ph -> ( ( X e. A /\ ( F ` X ) e. ( _V \ { Z } ) ) -> X e. W ) )
19	18	expdimp	|- ( ( ph /\ X e. A ) -> ( ( F ` X ) e. ( _V \ { Z } ) -> X e. W ) )
20	8 19	biimtrrid	|- ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z -> X e. W ) )
21	20	necon1bd	|- ( ( ph /\ X e. A ) -> ( -. X e. W -> ( F ` X ) = Z ) )
22	21	impr	|- ( ( ph /\ ( X e. A /\ -. X e. W ) ) -> ( F ` X ) = Z )
23	5 22	sylan2b	|- ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )