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 biimtrid 
 |-  ( ( ( 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 )