Metamath Proof Explorer

Theorem fvn0fvelrnOLD

Description: Obsolete version of fvn0fvelrn as of 13-Jan-2025. (Contributed by Alexander van der Vekens, 22-Jul-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion fvn0fvelrnOLD 
|- ( ( F ` X ) =/= (/) -> ( F ` X ) e. ran F )

Proof

Step Hyp Ref Expression
1 fvfundmfvn0 
 |-  ( ( F ` X ) =/= (/) -> ( X e. dom F /\ Fun ( F |` { X } ) ) )
2 eldmressnsn 
 |-  ( X e. dom F -> X e. dom ( F |` { X } ) )
3 fvelrn 
 |-  ( ( Fun ( F |` { X } ) /\ X e. dom ( F |` { X } ) ) -> ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) )
4 pm3.2 
 |-  ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) -> ( X e. dom F -> ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) /\ X e. dom F ) ) )
5 3 4 syl 
 |-  ( ( Fun ( F |` { X } ) /\ X e. dom ( F |` { X } ) ) -> ( X e. dom F -> ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) /\ X e. dom F ) ) )
6 5 ex 
 |-  ( Fun ( F |` { X } ) -> ( X e. dom ( F |` { X } ) -> ( X e. dom F -> ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) /\ X e. dom F ) ) ) )
7 6 com13 
 |-  ( X e. dom F -> ( X e. dom ( F |` { X } ) -> ( Fun ( F |` { X } ) -> ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) /\ X e. dom F ) ) ) )
8 2 7 mpd 
 |-  ( X e. dom F -> ( Fun ( F |` { X } ) -> ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) /\ X e. dom F ) ) )
9 8 imp 
 |-  ( ( X e. dom F /\ Fun ( F |` { X } ) ) -> ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) /\ X e. dom F ) )
10 fvressn 
 |-  ( X e. dom F -> ( ( F |` { X } ) ` X ) = ( F ` X ) )
11 10 eleq1d 
 |-  ( X e. dom F -> ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) <-> ( F ` X ) e. ran ( F |` { X } ) ) )
12 fvrnressn 
 |-  ( X e. dom F -> ( ( F ` X ) e. ran ( F |` { X } ) -> ( F ` X ) e. ran F ) )
13 11 12 sylbid 
 |-  ( X e. dom F -> ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) -> ( F ` X ) e. ran F ) )
14 13 impcom 
 |-  ( ( ( ( F |` { X } ) ` X ) e. ran ( F |` { X } ) /\ X e. dom F ) -> ( F ` X ) e. ran F )
15 1 9 14 3syl 
 |-  ( ( F ` X ) =/= (/) -> ( F ` X ) e. ran F )