ex-rn

Description: Example for df-rn . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

		Ref	Expression
	Assertion	ex-rn	$⊢ F = \{⟨2, 6⟩, ⟨3, 9⟩\} \to ran F = \{6, 9\}$

Step	Hyp	Ref	Expression
1		rneq	$⊢ F = \{⟨2, 6⟩, ⟨3, 9⟩\} \to ran F = ran \{⟨2, 6⟩, ⟨3, 9⟩\}$
2		df-pr	$⊢ \{⟨2, 6⟩, ⟨3, 9⟩\} = \{⟨2, 6⟩\} \cup \{⟨3, 9⟩\}$
3	2	rneqi	$⊢ ran \{⟨2, 6⟩, ⟨3, 9⟩\} = ran (\{⟨2, 6⟩\} \cup \{⟨3, 9⟩\})$
4		rnun	$⊢ ran (\{⟨2, 6⟩\} \cup \{⟨3, 9⟩\}) = ran \{⟨2, 6⟩\} \cup ran \{⟨3, 9⟩\}$
5		2nn	$⊢ 2 \in ℕ$
6	5	elexi	$⊢ 2 \in V$
7	6	rnsnop	$⊢ ran \{⟨2, 6⟩\} = \{6\}$
8		3nn	$⊢ 3 \in ℕ$
9	8	elexi	$⊢ 3 \in V$
10	9	rnsnop	$⊢ ran \{⟨3, 9⟩\} = \{9\}$
11	7 10	uneq12i	$⊢ ran \{⟨2, 6⟩\} \cup ran \{⟨3, 9⟩\} = \{6\} \cup \{9\}$
12		df-pr	$⊢ \{6, 9\} = \{6\} \cup \{9\}$
13	11 12	eqtr4i	$⊢ ran \{⟨2, 6⟩\} \cup ran \{⟨3, 9⟩\} = \{6, 9\}$
14	3 4 13	3eqtri	$⊢ ran \{⟨2, 6⟩, ⟨3, 9⟩\} = \{6, 9\}$
15	1 14	eqtrdi	$⊢ F = \{⟨2, 6⟩, ⟨3, 9⟩\} \to ran F = \{6, 9\}$

Metamath Proof Explorer