Theorem rnfdmpr

Description: The range of a one-to-one function F of an unordered pair into a set is the unordered pair of the function values. (Contributed by Alexander van der Vekens, 2-Feb-2018)

	Ref	Expression
Assertion	rnfdmpr	$$⊢\left(X\in V\wedge Y\in W\right)\to \left(FFn\left\{X,Y\right\}\to \mathrm{ran}F=\left\{F\left(X\right),F\left(Y\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnrnfv	$$⊢FFn\left\{X,Y\right\}\to \mathrm{ran}F=\left\{x|\exists i\in \left\{X,Y\right\}x=F\left(i\right)\right\}$$
2	1	adantl	$$⊢\left(\left(X\in V\wedge Y\in W\right)\wedge FFn\left\{X,Y\right\}\right)\to \mathrm{ran}F=\left\{x|\exists i\in \left\{X,Y\right\}x=F\left(i\right)\right\}$$
3		fveq2	$$⊢i=X\to F\left(i\right)=F\left(X\right)$$
4	3	eqeq2d	$$⊢i=X\to \left(x=F\left(i\right)\leftrightarrow x=F\left(X\right)\right)$$
5	4	abbidv	$$⊢i=X\to \left\{x|x=F\left(i\right)\right\}=\left\{x|x=F\left(X\right)\right\}$$
6		fveq2	$$⊢i=Y\to F\left(i\right)=F\left(Y\right)$$
7	6	eqeq2d	$$⊢i=Y\to \left(x=F\left(i\right)\leftrightarrow x=F\left(Y\right)\right)$$
8	7	abbidv	$$⊢i=Y\to \left\{x|x=F\left(i\right)\right\}=\left\{x|x=F\left(Y\right)\right\}$$
9	5 8	iunxprg	$$⊢\left(X\in V\wedge Y\in W\right)\to \bigcup _{i\in \left\{X,Y\right\}}\left\{x|x=F\left(i\right)\right\}=\left\{x|x=F\left(X\right)\right\}\cup \left\{x|x=F\left(Y\right)\right\}$$
10	9	adantr	$$⊢\left(\left(X\in V\wedge Y\in W\right)\wedge FFn\left\{X,Y\right\}\right)\to \bigcup _{i\in \left\{X,Y\right\}}\left\{x|x=F\left(i\right)\right\}=\left\{x|x=F\left(X\right)\right\}\cup \left\{x|x=F\left(Y\right)\right\}$$
11		iunab	$$⊢\bigcup _{i\in \left\{X,Y\right\}}\left\{x|x=F\left(i\right)\right\}=\left\{x|\exists i\in \left\{X,Y\right\}x=F\left(i\right)\right\}$$
12		df-sn	$$⊢\left\{F\left(X\right)\right\}=\left\{x|x=F\left(X\right)\right\}$$
13	12	eqcomi	$$⊢\left\{x|x=F\left(X\right)\right\}=\left\{F\left(X\right)\right\}$$
14		df-sn	$$⊢\left\{F\left(Y\right)\right\}=\left\{x|x=F\left(Y\right)\right\}$$
15	14	eqcomi	$$⊢\left\{x|x=F\left(Y\right)\right\}=\left\{F\left(Y\right)\right\}$$
16	13 15	uneq12i	$$⊢\left\{x|x=F\left(X\right)\right\}\cup \left\{x|x=F\left(Y\right)\right\}=\left\{F\left(X\right)\right\}\cup \left\{F\left(Y\right)\right\}$$
17		df-pr	$$⊢\left\{F\left(X\right),F\left(Y\right)\right\}=\left\{F\left(X\right)\right\}\cup \left\{F\left(Y\right)\right\}$$
18	16 17	eqtr4i	$$⊢\left\{x|x=F\left(X\right)\right\}\cup \left\{x|x=F\left(Y\right)\right\}=\left\{F\left(X\right),F\left(Y\right)\right\}$$
19	10 11 18	3eqtr3g	$$⊢\left(\left(X\in V\wedge Y\in W\right)\wedge FFn\left\{X,Y\right\}\right)\to \left\{x|\exists i\in \left\{X,Y\right\}x=F\left(i\right)\right\}=\left\{F\left(X\right),F\left(Y\right)\right\}$$
20	2 19	eqtrd	$$⊢\left(\left(X\in V\wedge Y\in W\right)\wedge FFn\left\{X,Y\right\}\right)\to \mathrm{ran}F=\left\{F\left(X\right),F\left(Y\right)\right\}$$
21	20	ex	$$⊢\left(X\in V\wedge Y\in W\right)\to \left(FFn\left\{X,Y\right\}\to \mathrm{ran}F=\left\{F\left(X\right),F\left(Y\right)\right\}\right)$$