This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funeldmb

Description: If (/) is not part of the range of a function F , then A is in the domain of F iff ( FA ) =/= (/) . (Contributed by Scott Fenton, 7-Dec-2021)

Ref Expression
Assertion funeldmb 
|- ( ( Fun F /\ -. (/) e. ran F ) -> ( A e. dom F <-> ( F ` A ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 fvelrn 
 |-  ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )
2 1 ex 
 |-  ( Fun F -> ( A e. dom F -> ( F ` A ) e. ran F ) )
3 2 adantr 
 |-  ( ( Fun F /\ ( F ` A ) = (/) ) -> ( A e. dom F -> ( F ` A ) e. ran F ) )
4 eleq1 
 |-  ( ( F ` A ) = (/) -> ( ( F ` A ) e. ran F <-> (/) e. ran F ) )
5 4 adantl 
 |-  ( ( Fun F /\ ( F ` A ) = (/) ) -> ( ( F ` A ) e. ran F <-> (/) e. ran F ) )
6 3 5 sylibd 
 |-  ( ( Fun F /\ ( F ` A ) = (/) ) -> ( A e. dom F -> (/) e. ran F ) )
7 6 con3d 
 |-  ( ( Fun F /\ ( F ` A ) = (/) ) -> ( -. (/) e. ran F -> -. A e. dom F ) )
8 7 impancom 
 |-  ( ( Fun F /\ -. (/) e. ran F ) -> ( ( F ` A ) = (/) -> -. A e. dom F ) )
9 ndmfv 
 |-  ( -. A e. dom F -> ( F ` A ) = (/) )
10 8 9 impbid1 
 |-  ( ( Fun F /\ -. (/) e. ran F ) -> ( ( F ` A ) = (/) <-> -. A e. dom F ) )
11 10 necon2abid 
 |-  ( ( Fun F /\ -. (/) e. ran F ) -> ( A e. dom F <-> ( F ` A ) =/= (/) ) )