# Metamath Proof Explorer

## Theorem extmptsuppeq

Description: The support of an extended function is the same as the original. (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 30-Jun-2019)

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

### Proof

Step Hyp Ref Expression
1 extmptsuppeq.b ${⊢}{\phi }\to {B}\in {W}$
2 extmptsuppeq.a ${⊢}{\phi }\to {A}\subseteq {B}$
3 extmptsuppeq.z ${⊢}\left({\phi }\wedge {n}\in \left({B}\setminus {A}\right)\right)\to {X}={Z}$
4 2 adantl ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to {A}\subseteq {B}$
5 4 sseld ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left({n}\in {A}\to {n}\in {B}\right)$
6 5 anim1d ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left(\left({n}\in {A}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)\to \left({n}\in {B}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)\right)$
7 eldif ${⊢}{n}\in \left({B}\setminus {A}\right)↔\left({n}\in {B}\wedge ¬{n}\in {A}\right)$
8 3 adantll ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {n}\in \left({B}\setminus {A}\right)\right)\to {X}={Z}$
9 7 8 sylan2br ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge \left({n}\in {B}\wedge ¬{n}\in {A}\right)\right)\to {X}={Z}$
10 9 expr ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {n}\in {B}\right)\to \left(¬{n}\in {A}\to {X}={Z}\right)$
11 elsn2g ${⊢}{Z}\in \mathrm{V}\to \left({X}\in \left\{{Z}\right\}↔{X}={Z}\right)$
12 elndif ${⊢}{X}\in \left\{{Z}\right\}\to ¬{X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)$
13 11 12 syl6bir ${⊢}{Z}\in \mathrm{V}\to \left({X}={Z}\to ¬{X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)$
14 13 ad2antrr ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {n}\in {B}\right)\to \left({X}={Z}\to ¬{X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)$
15 10 14 syld ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {n}\in {B}\right)\to \left(¬{n}\in {A}\to ¬{X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)$
16 15 con4d ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge {n}\in {B}\right)\to \left({X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\to {n}\in {A}\right)$
17 16 impr ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge \left({n}\in {B}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)\right)\to {n}\in {A}$
18 simprr ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge \left({n}\in {B}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)\right)\to {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)$
19 17 18 jca ${⊢}\left(\left({Z}\in \mathrm{V}\wedge {\phi }\right)\wedge \left({n}\in {B}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)\right)\to \left({n}\in {A}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)$
20 19 ex ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left(\left({n}\in {B}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)\to \left({n}\in {A}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)\right)$
21 6 20 impbid ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left(\left({n}\in {A}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)↔\left({n}\in {B}\wedge {X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right)\right)$
22 21 rabbidva2 ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left\{{n}\in {A}|{X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right\}=\left\{{n}\in {B}|{X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right\}$
23 eqid ${⊢}\left({n}\in {A}⟼{X}\right)=\left({n}\in {A}⟼{X}\right)$
24 1 2 ssexd ${⊢}{\phi }\to {A}\in \mathrm{V}$
25 24 adantl ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to {A}\in \mathrm{V}$
26 simpl ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to {Z}\in \mathrm{V}$
27 23 25 26 mptsuppdifd ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left({n}\in {A}⟼{X}\right)\mathrm{supp}{Z}=\left\{{n}\in {A}|{X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right\}$
28 eqid ${⊢}\left({n}\in {B}⟼{X}\right)=\left({n}\in {B}⟼{X}\right)$
29 1 adantl ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to {B}\in {W}$
30 28 29 26 mptsuppdifd ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left({n}\in {B}⟼{X}\right)\mathrm{supp}{Z}=\left\{{n}\in {B}|{X}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right\}$
31 22 27 30 3eqtr4d ${⊢}\left({Z}\in \mathrm{V}\wedge {\phi }\right)\to \left({n}\in {A}⟼{X}\right)\mathrm{supp}{Z}=\left({n}\in {B}⟼{X}\right)\mathrm{supp}{Z}$
32 31 ex ${⊢}{Z}\in \mathrm{V}\to \left({\phi }\to \left({n}\in {A}⟼{X}\right)\mathrm{supp}{Z}=\left({n}\in {B}⟼{X}\right)\mathrm{supp}{Z}\right)$
33 simpr ${⊢}\left(\left({n}\in {A}⟼{X}\right)\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {Z}\in \mathrm{V}$
34 33 con3i ${⊢}¬{Z}\in \mathrm{V}\to ¬\left(\left({n}\in {A}⟼{X}\right)\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)$
35 supp0prc ${⊢}¬\left(\left({n}\in {A}⟼{X}\right)\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left({n}\in {A}⟼{X}\right)\mathrm{supp}{Z}=\varnothing$
36 34 35 syl ${⊢}¬{Z}\in \mathrm{V}\to \left({n}\in {A}⟼{X}\right)\mathrm{supp}{Z}=\varnothing$
37 simpr ${⊢}\left(\left({n}\in {B}⟼{X}\right)\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to {Z}\in \mathrm{V}$
38 37 con3i ${⊢}¬{Z}\in \mathrm{V}\to ¬\left(\left({n}\in {B}⟼{X}\right)\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)$
39 supp0prc ${⊢}¬\left(\left({n}\in {B}⟼{X}\right)\in \mathrm{V}\wedge {Z}\in \mathrm{V}\right)\to \left({n}\in {B}⟼{X}\right)\mathrm{supp}{Z}=\varnothing$
40 38 39 syl ${⊢}¬{Z}\in \mathrm{V}\to \left({n}\in {B}⟼{X}\right)\mathrm{supp}{Z}=\varnothing$
41 36 40 eqtr4d ${⊢}¬{Z}\in \mathrm{V}\to \left({n}\in {A}⟼{X}\right)\mathrm{supp}{Z}=\left({n}\in {B}⟼{X}\right)\mathrm{supp}{Z}$
42 41 a1d ${⊢}¬{Z}\in \mathrm{V}\to \left({\phi }\to \left({n}\in {A}⟼{X}\right)\mathrm{supp}{Z}=\left({n}\in {B}⟼{X}\right)\mathrm{supp}{Z}\right)$
43 32 42 pm2.61i ${⊢}{\phi }\to \left({n}\in {A}⟼{X}\right)\mathrm{supp}{Z}=\left({n}\in {B}⟼{X}\right)\mathrm{supp}{Z}$