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)

	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		fdm	\|- ( F : A --> B -> dom F = A )
6		dmexg	\|- ( F e. _V -> dom F e. _V )
7	6	adantr	\|- ( ( F e. _V /\ Z e. _V ) -> dom F e. _V )
8		eleq1	\|- ( A = dom F -> ( A e. _V <-> dom F e. _V ) )
9	8	eqcoms	\|- ( dom F = A -> ( A e. _V <-> dom F e. _V ) )
10	7 9	syl5ibr	\|- ( dom F = A -> ( ( F e. _V /\ Z e. _V ) -> A e. _V ) )
11	1 5 10	3syl	\|- ( ph -> ( ( F e. _V /\ Z e. _V ) -> A e. _V ) )
12	11	impcom	\|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> A e. _V )
13		simplr	\|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> Z e. _V )
14		elsuppfn	\|- ( ( F Fn A /\ A e. _V /\ Z e. _V ) -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )
15	4 12 13 14	syl3anc	\|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )
16		eldif	\|- ( k e. ( A \ W ) <-> ( k e. A /\ -. k e. W ) )
17	2	adantll	\|- ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )
18	16 17	sylan2br	\|- ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ ( k e. A /\ -. k e. W ) ) -> ( F ` k ) = Z )
19	18	expr	\|- ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. A ) -> ( -. k e. W -> ( F ` k ) = Z ) )
20	19	necon1ad	\|- ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. A ) -> ( ( F ` k ) =/= Z -> k e. W ) )
21	20	expimpd	\|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( ( k e. A /\ ( F ` k ) =/= Z ) -> k e. W ) )
22	15 21	sylbid	\|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( k e. ( F supp Z ) -> k e. W ) )
23	22	ssrdv	\|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( F supp Z ) C_ W )
24	23	ex	\|- ( ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ W ) )
25		supp0prc	\|- ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = (/) )
26		0ss	\|- (/) C_ W
27	25 26	eqsstrdi	\|- ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) C_ W )
28	27	a1d	\|- ( -. ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ W ) )
29	24 28	pm2.61i	\|- ( ph -> ( F supp Z ) C_ W )

Metamath Proof Explorer

Theorem suppss

Proof