# Metamath Proof Explorer

## Theorem suppdm

Description: If the range of a function does not contain the zero, the support of the function equals its domain. (Contributed by AV, 20-May-2020)

Ref Expression
Assertion suppdm ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {Z}\notin \mathrm{ran}{F}\right)\to {F}\mathrm{supp}{Z}=\mathrm{dom}{F}$

### Proof

Step Hyp Ref Expression
1 suppval1 ${⊢}\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\to {F}\mathrm{supp}{Z}=\left\{{x}\in \mathrm{dom}{F}|{F}\left({x}\right)\ne {Z}\right\}$
2 1 adantr ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {Z}\notin \mathrm{ran}{F}\right)\to {F}\mathrm{supp}{Z}=\left\{{x}\in \mathrm{dom}{F}|{F}\left({x}\right)\ne {Z}\right\}$
3 df-nel ${⊢}{Z}\notin \mathrm{ran}{F}↔¬{Z}\in \mathrm{ran}{F}$
4 fvelrn ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to {F}\left({x}\right)\in \mathrm{ran}{F}$
5 4 3ad2antl1 ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {x}\in \mathrm{dom}{F}\right)\to {F}\left({x}\right)\in \mathrm{ran}{F}$
6 eleq1 ${⊢}{Z}={F}\left({x}\right)\to \left({Z}\in \mathrm{ran}{F}↔{F}\left({x}\right)\in \mathrm{ran}{F}\right)$
7 6 eqcoms ${⊢}{F}\left({x}\right)={Z}\to \left({Z}\in \mathrm{ran}{F}↔{F}\left({x}\right)\in \mathrm{ran}{F}\right)$
8 5 7 syl5ibrcom ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {x}\in \mathrm{dom}{F}\right)\to \left({F}\left({x}\right)={Z}\to {Z}\in \mathrm{ran}{F}\right)$
9 8 necon3bd ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {x}\in \mathrm{dom}{F}\right)\to \left(¬{Z}\in \mathrm{ran}{F}\to {F}\left({x}\right)\ne {Z}\right)$
10 3 9 syl5bi ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {x}\in \mathrm{dom}{F}\right)\to \left({Z}\notin \mathrm{ran}{F}\to {F}\left({x}\right)\ne {Z}\right)$
11 10 impancom ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {Z}\notin \mathrm{ran}{F}\right)\to \left({x}\in \mathrm{dom}{F}\to {F}\left({x}\right)\ne {Z}\right)$
12 11 ralrimiv ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {Z}\notin \mathrm{ran}{F}\right)\to \forall {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\ne {Z}$
13 rabid2 ${⊢}\mathrm{dom}{F}=\left\{{x}\in \mathrm{dom}{F}|{F}\left({x}\right)\ne {Z}\right\}↔\forall {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\ne {Z}$
14 12 13 sylibr ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {Z}\notin \mathrm{ran}{F}\right)\to \mathrm{dom}{F}=\left\{{x}\in \mathrm{dom}{F}|{F}\left({x}\right)\ne {Z}\right\}$
15 2 14 eqtr4d ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {F}\in {V}\wedge {Z}\in {W}\right)\wedge {Z}\notin \mathrm{ran}{F}\right)\to {F}\mathrm{supp}{Z}=\mathrm{dom}{F}$