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 Fun F F V Z W Z ran F F supp Z = dom F

Proof

Step Hyp Ref Expression
1 suppval1 Fun F F V Z W F supp Z = x dom F | F x Z
2 1 adantr Fun F F V Z W Z ran F F supp Z = x dom F | F x Z
3 df-nel Z ran F ¬ Z ran F
4 fvelrn Fun F x dom F F x ran F
5 4 3ad2antl1 Fun F F V Z W x dom F F x ran F
6 eleq1 Z = F x Z ran F F x ran F
7 6 eqcoms F x = Z Z ran F F x ran F
8 5 7 syl5ibrcom Fun F F V Z W x dom F F x = Z Z ran F
9 8 necon3bd Fun F F V Z W x dom F ¬ Z ran F F x Z
10 3 9 syl5bi Fun F F V Z W x dom F Z ran F F x Z
11 10 impancom Fun F F V Z W Z ran F x dom F F x Z
12 11 ralrimiv Fun F F V Z W Z ran F x dom F F x Z
13 rabid2 dom F = x dom F | F x Z x dom F F x Z
14 12 13 sylibr Fun F F V Z W Z ran F dom F = x dom F | F x Z
15 2 14 eqtr4d Fun F F V Z W Z ran F F supp Z = dom F