Theorem 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=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to \mathrm{ran}F=\left\{6,9\right\}$$

Proof

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