# Metamath Proof Explorer

## Theorem suppss2

Description: Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 22-Mar-2015) (Revised by AV, 28-May-2019)

Ref Expression
Hypotheses suppss2.n ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {W}\right)\right)\to {B}={Z}$
suppss2.a ${⊢}{\phi }\to {A}\in {V}$
Assertion suppss2 ${⊢}{\phi }\to \left({k}\in {A}⟼{B}\right)\mathrm{supp}{Z}\subseteq {W}$

### Proof

Step Hyp Ref Expression
1 suppss2.n ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {W}\right)\right)\to {B}={Z}$
2 suppss2.a ${⊢}{\phi }\to {A}\in {V}$
3 eqid ${⊢}\left({k}\in {A}⟼{B}\right)=\left({k}\in {A}⟼{B}\right)$
4 2 adantl ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to {A}\in {V}$
5 simpl ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to {Z}\in \mathrm{V}$
6 3 4 5 mptsuppdifd ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left({k}\in {A}⟼{B}\right)\mathrm{supp}{Z}=\left\{{k}\in {A}|{B}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right\}$
7 eldifsni ${⊢}{B}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\to {B}\ne {Z}$
8 eldif ${⊢}{k}\in \left({A}\setminus {W}\right)↔\left({k}\in {A}\wedge ¬{k}\in {W}\right)$
9 1 adantll ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {k}\in \left({A}\setminus {W}\right)\right)\to {B}={Z}$
10 8 9 sylan2br ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge \left({k}\in {A}\wedge ¬{k}\in {W}\right)\right)\to {B}={Z}$
11 10 expr ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {k}\in {A}\right)\to \left(¬{k}\in {W}\to {B}={Z}\right)$
12 11 necon1ad ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {k}\in {A}\right)\to \left({B}\ne {Z}\to {k}\in {W}\right)$
13 7 12 syl5 ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {k}\in {A}\right)\to \left({B}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\to {k}\in {W}\right)$
14 13 3impia ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {k}\in {A}\wedge {B}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)\to {k}\in {W}$
15 14 rabssdv ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left\{{k}\in {A}|{B}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right\}\subseteq {W}$
16 6 15 eqsstrd ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left({k}\in {A}⟼{B}\right)\mathrm{supp}{Z}\subseteq {W}$
17 16 ex ${⊢}{Z}\in \mathrm{V}\to \left({\phi }\to \left({k}\in {A}⟼{B}\right)\mathrm{supp}{Z}\subseteq {W}\right)$
18 id ${⊢}¬{Z}\in \mathrm{V}\to ¬{Z}\in \mathrm{V}$
19 18 intnand ${⊢}¬{Z}\in \mathrm{V}\to ¬\left(\left({k}\in {A}⟼{B}\right)\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)$
20 supp0prc ${⊢}¬\left(\left({k}\in {A}⟼{B}\right)\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left({k}\in {A}⟼{B}\right)\mathrm{supp}{Z}=\varnothing$
21 19 20 syl ${⊢}¬{Z}\in \mathrm{V}\to \left({k}\in {A}⟼{B}\right)\mathrm{supp}{Z}=\varnothing$
22 0ss ${⊢}\varnothing \subseteq {W}$
23 21 22 eqsstrdi ${⊢}¬{Z}\in \mathrm{V}\to \left({k}\in {A}⟼{B}\right)\mathrm{supp}{Z}\subseteq {W}$
24 23 a1d ${⊢}¬{Z}\in \mathrm{V}\to \left({\phi }\to \left({k}\in {A}⟼{B}\right)\mathrm{supp}{Z}\subseteq {W}\right)$
25 17 24 pm2.61i ${⊢}{\phi }\to \left({k}\in {A}⟼{B}\right)\mathrm{supp}{Z}\subseteq {W}$