# Metamath Proof Explorer

## Theorem fnsuppeq0

Description: The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015) (Revised by AV, 28-May-2019)

Ref Expression
Assertion fnsuppeq0 ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to \left({F}\mathrm{supp}{Z}=\varnothing ↔{F}={A}×\left\{{Z}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 ss0b ${⊢}{F}\mathrm{supp}{Z}\subseteq \varnothing ↔{F}\mathrm{supp}{Z}=\varnothing$
2 un0 ${⊢}{A}\cup \varnothing ={A}$
3 uncom ${⊢}{A}\cup \varnothing =\varnothing \cup {A}$
4 2 3 eqtr3i ${⊢}{A}=\varnothing \cup {A}$
5 4 fneq2i ${⊢}{F}Fn{A}↔{F}Fn\left(\varnothing \cup {A}\right)$
6 5 biimpi ${⊢}{F}Fn{A}\to {F}Fn\left(\varnothing \cup {A}\right)$
7 6 3ad2ant1 ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to {F}Fn\left(\varnothing \cup {A}\right)$
8 fnex ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\right)\to {F}\in \mathrm{V}$
9 8 3adant3 ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to {F}\in \mathrm{V}$
10 simp3 ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to {Z}\in {V}$
11 0in ${⊢}\varnothing \cap {A}=\varnothing$
12 11 a1i ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to \varnothing \cap {A}=\varnothing$
13 fnsuppres ${⊢}\left({F}Fn\left(\varnothing \cup {A}\right)\wedge \left({F}\in \mathrm{V}\wedge {Z}\in {V}\right)\wedge \varnothing \cap {A}=\varnothing \right)\to \left({F}\mathrm{supp}{Z}\subseteq \varnothing ↔{{F}↾}_{{A}}={A}×\left\{{Z}\right\}\right)$
14 7 9 10 12 13 syl121anc ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to \left({F}\mathrm{supp}{Z}\subseteq \varnothing ↔{{F}↾}_{{A}}={A}×\left\{{Z}\right\}\right)$
15 1 14 syl5bbr ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to \left({F}\mathrm{supp}{Z}=\varnothing ↔{{F}↾}_{{A}}={A}×\left\{{Z}\right\}\right)$
16 fnresdm ${⊢}{F}Fn{A}\to {{F}↾}_{{A}}={F}$
17 16 3ad2ant1 ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to {{F}↾}_{{A}}={F}$
18 17 eqeq1d ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to \left({{F}↾}_{{A}}={A}×\left\{{Z}\right\}↔{F}={A}×\left\{{Z}\right\}\right)$
19 15 18 bitrd ${⊢}\left({F}Fn{A}\wedge {A}\in {W}\wedge {Z}\in {V}\right)\to \left({F}\mathrm{supp}{Z}=\varnothing ↔{F}={A}×\left\{{Z}\right\}\right)$