Metamath Proof Explorer

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) \neq \emptyset \to F (X) \in ran F$

Proof

Step	Hyp	Ref	Expression
1		fvfundmfvn0	$⊢ F (X) \neq \emptyset \to (X \in dom F \land Fun ({F ↾}_{\{X\}}))$
2		eldmressnsn	$⊢ X \in dom F \to X \in dom ({F ↾}_{\{X\}})$
3		fvelrn	$⊢ (Fun ({F ↾}_{\{X\}}) \land X \in dom ({F ↾}_{\{X\}})) \to ({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}})$
4		pm3.2	$⊢ ({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \to (X \in dom F \to (({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \land X \in dom F))$
5	3 4	syl	$⊢ (Fun ({F ↾}_{\{X\}}) \land X \in dom ({F ↾}_{\{X\}})) \to (X \in dom F \to (({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \land X \in dom F))$
6	5	ex	$⊢ Fun ({F ↾}_{\{X\}}) \to (X \in dom ({F ↾}_{\{X\}}) \to (X \in dom F \to (({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \land X \in dom F)))$
7	6	com13	$⊢ X \in dom F \to (X \in dom ({F ↾}_{\{X\}}) \to (Fun ({F ↾}_{\{X\}}) \to (({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \land X \in dom F)))$
8	2 7	mpd	$⊢ X \in dom F \to (Fun ({F ↾}_{\{X\}}) \to (({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \land X \in dom F))$
9	8	imp	$⊢ (X \in dom F \land Fun ({F ↾}_{\{X\}})) \to (({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \land X \in dom F)$
10		fvressn	$⊢ X \in dom F \to ({F ↾}_{\{X\}}) (X) = F (X)$
11	10	eleq1d	$⊢ X \in dom F \to (({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \leftrightarrow F (X) \in ran ({F ↾}_{\{X\}}))$
12		fvrnressn	$⊢ X \in dom F \to (F (X) \in ran ({F ↾}_{\{X\}}) \to F (X) \in ran F)$
13	11 12	sylbid	$⊢ X \in dom F \to (({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \to F (X) \in ran F)$
14	13	impcom	$⊢ (({F ↾}_{\{X\}}) (X) \in ran ({F ↾}_{\{X\}}) \land X \in dom F) \to F (X) \in ran F$
15	1 9 14	3syl	$⊢ F (X) \neq \emptyset \to F (X) \in ran F$