Metamath Proof Explorer

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)

Ref Expression
Hypotheses suppss.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
suppss.n ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {W}\right)\right)\to {F}\left({k}\right)={Z}$
Assertion suppss ${⊢}{\phi }\to {F}\mathrm{supp}{Z}\subseteq {W}$

Proof

Step Hyp Ref Expression
1 suppss.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
2 suppss.n ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {W}\right)\right)\to {F}\left({k}\right)={Z}$
3 1 ffnd ${⊢}{\phi }\to {F}Fn{A}$
4 3 adantl ${⊢}\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\to {F}Fn{A}$
5 fdm ${⊢}{F}:{A}⟶{B}\to \mathrm{dom}{F}={A}$
6 dmexg ${⊢}{F}\in \mathrm{V}\to \mathrm{dom}{F}\in \mathrm{V}$
7 6 adantr ${⊢}\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \mathrm{dom}{F}\in \mathrm{V}$
8 eleq1 ${⊢}{A}=\mathrm{dom}{F}\to \left({A}\in \mathrm{V}↔\mathrm{dom}{F}\in \mathrm{V}\right)$
9 8 eqcoms ${⊢}\mathrm{dom}{F}={A}\to \left({A}\in \mathrm{V}↔\mathrm{dom}{F}\in \mathrm{V}\right)$
10 7 9 syl5ibr ${⊢}\mathrm{dom}{F}={A}\to \left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {A}\in \mathrm{V}\right)$
11 1 5 10 3syl ${⊢}{\phi }\to \left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {A}\in \mathrm{V}\right)$
12 11 impcom ${⊢}\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\to {A}\in \mathrm{V}$
13 simplr ${⊢}\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\to {Z}\in \mathrm{V}$
14 elsuppfn ${⊢}\left({F}Fn{A}\wedge {A}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left({k}\in {supp}_{{Z}}\left({F}\right)↔\left({k}\in {A}\wedge {F}\left({k}\right)\ne {Z}\right)\right)$
15 4 12 13 14 syl3anc ${⊢}\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\to \left({k}\in {supp}_{{Z}}\left({F}\right)↔\left({k}\in {A}\wedge {F}\left({k}\right)\ne {Z}\right)\right)$
16 eldif ${⊢}{k}\in \left({A}\setminus {W}\right)↔\left({k}\in {A}\wedge ¬{k}\in {W}\right)$
17 2 adantll ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\wedge {k}\in \left({A}\setminus {W}\right)\right)\to {F}\left({k}\right)={Z}$
18 16 17 sylan2br ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\wedge \left({k}\in {A}\wedge ¬{k}\in {W}\right)\right)\to {F}\left({k}\right)={Z}$
19 18 expr ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\wedge {k}\in {A}\right)\to \left(¬{k}\in {W}\to {F}\left({k}\right)={Z}\right)$
20 19 necon1ad ${⊢}\left(\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\wedge {k}\in {A}\right)\to \left({F}\left({k}\right)\ne {Z}\to {k}\in {W}\right)$
21 20 expimpd ${⊢}\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\to \left(\left({k}\in {A}\wedge {F}\left({k}\right)\ne {Z}\right)\to {k}\in {W}\right)$
22 15 21 sylbid ${⊢}\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\to \left({k}\in {supp}_{{Z}}\left({F}\right)\to {k}\in {W}\right)$
23 22 ssrdv ${⊢}\left(\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\wedge {\phi }\right)\to {F}\mathrm{supp}{Z}\subseteq {W}$
24 23 ex ${⊢}\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left({\phi }\to {F}\mathrm{supp}{Z}\subseteq {W}\right)$
25 supp0prc ${⊢}¬\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {F}\mathrm{supp}{Z}=\varnothing$
26 0ss ${⊢}\varnothing \subseteq {W}$
27 25 26 eqsstrdi ${⊢}¬\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {F}\mathrm{supp}{Z}\subseteq {W}$
28 27 a1d ${⊢}¬\left({F}\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left({\phi }\to {F}\mathrm{supp}{Z}\subseteq {W}\right)$
29 24 28 pm2.61i ${⊢}{\phi }\to {F}\mathrm{supp}{Z}\subseteq {W}$