# Metamath Proof Explorer

## Theorem suppfnss

Description: The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019) (Proof shortened by AV, 6-Jun-2022)

Ref Expression
Assertion suppfnss ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\to {F}\mathrm{supp}{Z}\subseteq {G}\mathrm{supp}{Z}\right)$

### Proof

Step Hyp Ref Expression
1 simpr1 ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to {A}\subseteq {B}$
2 fndm ${⊢}{F}Fn{A}\to \mathrm{dom}{F}={A}$
3 2 ad2antrr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \mathrm{dom}{F}={A}$
4 fndm ${⊢}{G}Fn{B}\to \mathrm{dom}{G}={B}$
5 4 ad2antlr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \mathrm{dom}{G}={B}$
6 1 3 5 3sstr4d ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \mathrm{dom}{F}\subseteq \mathrm{dom}{G}$
7 6 adantr ${⊢}\left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\right)\to \mathrm{dom}{F}\subseteq \mathrm{dom}{G}$
8 2 eleq2d ${⊢}{F}Fn{A}\to \left({y}\in \mathrm{dom}{F}↔{y}\in {A}\right)$
9 8 ad2antrr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \left({y}\in \mathrm{dom}{F}↔{y}\in {A}\right)$
10 fveqeq2 ${⊢}{x}={y}\to \left({G}\left({x}\right)={Z}↔{G}\left({y}\right)={Z}\right)$
11 fveqeq2 ${⊢}{x}={y}\to \left({F}\left({x}\right)={Z}↔{F}\left({y}\right)={Z}\right)$
12 10 11 imbi12d ${⊢}{x}={y}\to \left(\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)↔\left({G}\left({y}\right)={Z}\to {F}\left({y}\right)={Z}\right)\right)$
13 12 rspcv ${⊢}{y}\in {A}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\to \left({G}\left({y}\right)={Z}\to {F}\left({y}\right)={Z}\right)\right)$
14 9 13 syl6bi ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \left({y}\in \mathrm{dom}{F}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\to \left({G}\left({y}\right)={Z}\to {F}\left({y}\right)={Z}\right)\right)\right)$
15 14 com23 ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\to \left({y}\in \mathrm{dom}{F}\to \left({G}\left({y}\right)={Z}\to {F}\left({y}\right)={Z}\right)\right)\right)$
16 15 imp31 ${⊢}\left(\left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\right)\wedge {y}\in \mathrm{dom}{F}\right)\to \left({G}\left({y}\right)={Z}\to {F}\left({y}\right)={Z}\right)$
17 16 necon3d ${⊢}\left(\left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\right)\wedge {y}\in \mathrm{dom}{F}\right)\to \left({F}\left({y}\right)\ne {Z}\to {G}\left({y}\right)\ne {Z}\right)$
18 17 ex ${⊢}\left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\right)\to \left({y}\in \mathrm{dom}{F}\to \left({F}\left({y}\right)\ne {Z}\to {G}\left({y}\right)\ne {Z}\right)\right)$
19 18 com23 ${⊢}\left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\right)\to \left({F}\left({y}\right)\ne {Z}\to \left({y}\in \mathrm{dom}{F}\to {G}\left({y}\right)\ne {Z}\right)\right)$
20 19 3imp ${⊢}\left(\left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\right)\wedge {F}\left({y}\right)\ne {Z}\wedge {y}\in \mathrm{dom}{F}\right)\to {G}\left({y}\right)\ne {Z}$
21 7 20 rabssrabd ${⊢}\left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\right)\to \left\{{y}\in \mathrm{dom}{F}|{F}\left({y}\right)\ne {Z}\right\}\subseteq \left\{{y}\in \mathrm{dom}{G}|{G}\left({y}\right)\ne {Z}\right\}$
22 fnfun ${⊢}{F}Fn{A}\to \mathrm{Fun}{F}$
23 22 ad2antrr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \mathrm{Fun}{F}$
24 simpl ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to {F}Fn{A}$
25 ssexg ${⊢}\left({A}\subseteq {B}\wedge {B}\in {V}\right)\to {A}\in \mathrm{V}$
26 25 3adant3 ${⊢}\left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\to {A}\in \mathrm{V}$
27 fnex ${⊢}\left({F}Fn{A}\wedge {A}\in \mathrm{V}\right)\to {F}\in \mathrm{V}$
28 24 26 27 syl2an ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to {F}\in \mathrm{V}$
29 simpr3 ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to {Z}\in {W}$
30 suppval1 ${⊢}\left(\mathrm{Fun}{F}\wedge {F}\in \mathrm{V}\wedge {Z}\in {W}\right)\to {F}\mathrm{supp}{Z}=\left\{{y}\in \mathrm{dom}{F}|{F}\left({y}\right)\ne {Z}\right\}$
31 23 28 29 30 syl3anc ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to {F}\mathrm{supp}{Z}=\left\{{y}\in \mathrm{dom}{F}|{F}\left({y}\right)\ne {Z}\right\}$
32 fnfun ${⊢}{G}Fn{B}\to \mathrm{Fun}{G}$
33 32 ad2antlr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \mathrm{Fun}{G}$
34 simpr ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to {G}Fn{B}$
35 simp2 ${⊢}\left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\to {B}\in {V}$
36 fnex ${⊢}\left({G}Fn{B}\wedge {B}\in {V}\right)\to {G}\in \mathrm{V}$
37 34 35 36 syl2an ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to {G}\in \mathrm{V}$
38 suppval1 ${⊢}\left(\mathrm{Fun}{G}\wedge {G}\in \mathrm{V}\wedge {Z}\in {W}\right)\to {G}\mathrm{supp}{Z}=\left\{{y}\in \mathrm{dom}{G}|{G}\left({y}\right)\ne {Z}\right\}$
39 33 37 29 38 syl3anc ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to {G}\mathrm{supp}{Z}=\left\{{y}\in \mathrm{dom}{G}|{G}\left({y}\right)\ne {Z}\right\}$
40 31 39 sseq12d ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \left({F}\mathrm{supp}{Z}\subseteq {G}\mathrm{supp}{Z}↔\left\{{y}\in \mathrm{dom}{F}|{F}\left({y}\right)\ne {Z}\right\}\subseteq \left\{{y}\in \mathrm{dom}{G}|{G}\left({y}\right)\ne {Z}\right\}\right)$
41 40 adantr ${⊢}\left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\right)\to \left({F}\mathrm{supp}{Z}\subseteq {G}\mathrm{supp}{Z}↔\left\{{y}\in \mathrm{dom}{F}|{F}\left({y}\right)\ne {Z}\right\}\subseteq \left\{{y}\in \mathrm{dom}{G}|{G}\left({y}\right)\ne {Z}\right\}\right)$
42 21 41 mpbird ${⊢}\left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\right)\to {F}\mathrm{supp}{Z}\subseteq {G}\mathrm{supp}{Z}$
43 42 ex ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left({A}\subseteq {B}\wedge {B}\in {V}\wedge {Z}\in {W}\right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({G}\left({x}\right)={Z}\to {F}\left({x}\right)={Z}\right)\to {F}\mathrm{supp}{Z}\subseteq {G}\mathrm{supp}{Z}\right)$