Metamath Proof Explorer

Theorem fvrn0

Description: A function value is a member of the range plus null. (Contributed by Scott Fenton, 8-Jun-2011) (Revised by Stefan O'Rear, 3-Jan-2015)

		Ref	Expression
	Assertion	fvrn0	$⊢ F (X) \in (ran F \cup \{\emptyset\})$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ F (X) = \emptyset \to F (X) = \emptyset$
2		ssun2	$⊢ \{\emptyset\} \subseteq ran F \cup \{\emptyset\}$
3		0ex	$⊢ \emptyset \in V$
4	3	snid	$⊢ \emptyset \in \{\emptyset\}$
5	2 4	sselii	$⊢ \emptyset \in (ran F \cup \{\emptyset\})$
6	1 5	eqeltrdi	$⊢ F (X) = \emptyset \to F (X) \in (ran F \cup \{\emptyset\})$
7		ssun1	$⊢ ran F \subseteq ran F \cup \{\emptyset\}$
8		fvprc	$⊢ \neg X \in V \to F (X) = \emptyset$
9	8	con1i	$⊢ \neg F (X) = \emptyset \to X \in V$
10		fvexd	$⊢ \neg F (X) = \emptyset \to F (X) \in V$
11		fvbr0	$⊢ (X F F (X) \lor F (X) = \emptyset)$
12	11	ori	$⊢ \neg X F F (X) \to F (X) = \emptyset$
13	12	con1i	$⊢ \neg F (X) = \emptyset \to X F F (X)$
14		brelrng	$⊢ (X \in V \land F (X) \in V \land X F F (X)) \to F (X) \in ran F$
15	9 10 13 14	syl3anc	$⊢ \neg F (X) = \emptyset \to F (X) \in ran F$
16	7 15	sselid	$⊢ \neg F (X) = \emptyset \to F (X) \in (ran F \cup \{\emptyset\})$
17	6 16	pm2.61i	$⊢ F (X) \in (ran F \cup \{\emptyset\})$