Theorem fvn0fvelrn

Description: If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018)

	Ref	Expression
Assertion	fvn0fvelrn	|- ( ( 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 )