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 e. V /\ Z e. W ) /\ Z e/ ran F ) -> ( F supp Z ) = dom F )

Proof

Step Hyp Ref Expression
1 suppval1
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { x e. dom F | ( F ` x ) =/= Z } )
2 1 adantr
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> ( F supp Z ) = { x e. dom F | ( F ` x ) =/= Z } )
3 df-nel
 |-  ( Z e/ ran F <-> -. Z e. ran F )
4 fvelrn
 |-  ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F )
5 4 3ad2antl1
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( F ` x ) e. ran F )
6 eleq1
 |-  ( Z = ( F ` x ) -> ( Z e. ran F <-> ( F ` x ) e. ran F ) )
7 6 eqcoms
 |-  ( ( F ` x ) = Z -> ( Z e. ran F <-> ( F ` x ) e. ran F ) )
8 5 7 syl5ibrcom
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( ( F ` x ) = Z -> Z e. ran F ) )
9 8 necon3bd
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( -. Z e. ran F -> ( F ` x ) =/= Z ) )
10 3 9 syl5bi
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( Z e/ ran F -> ( F ` x ) =/= Z ) )
11 10 impancom
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> ( x e. dom F -> ( F ` x ) =/= Z ) )
12 11 ralrimiv
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> A. x e. dom F ( F ` x ) =/= Z )
13 rabid2
 |-  ( dom F = { x e. dom F | ( F ` x ) =/= Z } <-> A. x e. dom F ( F ` x ) =/= Z )
14 12 13 sylibr
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> dom F = { x e. dom F | ( F ` x ) =/= Z } )
15 2 14 eqtr4d
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> ( F supp Z ) = dom F )