Theorem suppss

Description: Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019) (Proof shortened by SN, 5-Aug-2024)

	Ref	Expression
Hypotheses	suppss.f	|- ( ph -> F : A --> B )
	suppss.n	|- ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )
Assertion	suppss	|- ( ph -> ( F supp Z ) C_ W )

Proof

Step	Hyp	Ref	Expression
1		suppss.f	|- ( ph -> F : A --> B )
2		suppss.n	|- ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )
3	1	ffnd	|- ( ph -> F Fn A )
4	3	adantl	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> F Fn A )
5		simpll	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> F e. _V )
6		simplr	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> Z e. _V )
7		elsuppfng	|- ( ( F Fn A /\ F e. _V /\ Z e. _V ) -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )
8	4 5 6 7	syl3anc	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )
9		eldif	|- ( k e. ( A \ W ) <-> ( k e. A /\ -. k e. W ) )
10	2	adantll	|- ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )
11	9 10	sylan2br	|- ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ ( k e. A /\ -. k e. W ) ) -> ( F ` k ) = Z )
12	11	expr	|- ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. A ) -> ( -. k e. W -> ( F ` k ) = Z ) )
13	12	necon1ad	|- ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. A ) -> ( ( F ` k ) =/= Z -> k e. W ) )
14	13	expimpd	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( ( k e. A /\ ( F ` k ) =/= Z ) -> k e. W ) )
15	8 14	sylbid	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( k e. ( F supp Z ) -> k e. W ) )
16	15	ssrdv	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( F supp Z ) C_ W )
17	16	ex	|- ( ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ W ) )
18		supp0prc	|- ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = (/) )
19		0ss	|- (/) C_ W
20	18 19	eqsstrdi	|- ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) C_ W )
21	20	a1d	|- ( -. ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ W ) )
22	17 21	pm2.61i	|- ( ph -> ( F supp Z ) C_ W )