Metamath Proof Explorer

Theorem feldmfvelcdm

Description: A class is an element of the domain iff it's function value is an element of the codomain of a function. (Contributed by AV, 22-Apr-2025)

Ref Expression
Assertion feldmfvelcdm 
|- ( ( F : A --> B /\ (/) e/ B ) -> ( X e. A <-> ( F ` X ) e. B ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( F : A --> B /\ (/) e/ B ) -> F : A --> B )
2 1 ffvelcdmda 
 |-  ( ( ( F : A --> B /\ (/) e/ B ) /\ X e. A ) -> ( F ` X ) e. B )
3 2 ex 
 |-  ( ( F : A --> B /\ (/) e/ B ) -> ( X e. A -> ( F ` X ) e. B ) )
4 df-nel 
 |-  ( (/) e/ B <-> -. (/) e. B )
5 nelelne 
 |-  ( -. (/) e. B -> ( ( F ` X ) e. B -> ( F ` X ) =/= (/) ) )
6 4 5 sylbi 
 |-  ( (/) e/ B -> ( ( F ` X ) e. B -> ( F ` X ) =/= (/) ) )
7 fdm 
 |-  ( F : A --> B -> dom F = A )
8 fvfundmfvn0 
 |-  ( ( F ` X ) =/= (/) -> ( X e. dom F /\ Fun ( F |` { X } ) ) )
9 simprl 
 |-  ( ( dom F = A /\ ( X e. dom F /\ Fun ( F |` { X } ) ) ) -> X e. dom F )
10 simpl 
 |-  ( ( dom F = A /\ ( X e. dom F /\ Fun ( F |` { X } ) ) ) -> dom F = A )
11 9 10 eleqtrd 
 |-  ( ( dom F = A /\ ( X e. dom F /\ Fun ( F |` { X } ) ) ) -> X e. A )
12 11 ex 
 |-  ( dom F = A -> ( ( X e. dom F /\ Fun ( F |` { X } ) ) -> X e. A ) )
13 7 8 12 syl2im 
 |-  ( F : A --> B -> ( ( F ` X ) =/= (/) -> X e. A ) )
14 6 13 sylan9r 
 |-  ( ( F : A --> B /\ (/) e/ B ) -> ( ( F ` X ) e. B -> X e. A ) )
15 3 14 impbid 
 |-  ( ( F : A --> B /\ (/) e/ B ) -> ( X e. A <-> ( F ` X ) e. B ) )