Theorem suppssrg

Description: A function is zero outside its support. Version of suppssr avoiding ax-rep by assuming F is a set rather than its domain A . (Contributed by SN, 5-May-2024)

	Ref	Expression
Hypotheses	suppssrg.f	|- ( ph -> F : A --> B )
	suppssrg.n	|- ( ph -> ( F supp Z ) C_ W )
	suppssrg.a	|- ( ph -> F e. V )
	suppssrg.z	|- ( ph -> Z e. U )
Assertion	suppssrg	|- ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )

Proof

Step	Hyp	Ref	Expression
1		suppssrg.f	|- ( ph -> F : A --> B )
2		suppssrg.n	|- ( ph -> ( F supp Z ) C_ W )
3		suppssrg.a	|- ( ph -> F e. V )
4		suppssrg.z	|- ( ph -> Z e. U )
5		eldif	|- ( X e. ( A \ W ) <-> ( X e. A /\ -. X e. W ) )
6	1	ffnd	|- ( ph -> F Fn A )
7		elsuppfng	|- ( ( F Fn A /\ F e. V /\ Z e. U ) -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
8	6 3 4 7	syl3anc	|- ( ph -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
9	2	sseld	|- ( ph -> ( X e. ( F supp Z ) -> X e. W ) )
10	8 9	sylbird	|- ( ph -> ( ( X e. A /\ ( F ` X ) =/= Z ) -> X e. W ) )
11	10	expdimp	|- ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z -> X e. W ) )
12	11	necon1bd	|- ( ( ph /\ X e. A ) -> ( -. X e. W -> ( F ` X ) = Z ) )
13	12	impr	|- ( ( ph /\ ( X e. A /\ -. X e. W ) ) -> ( F ` X ) = Z )
14	5 13	sylan2b	|- ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )