Theorem fpr

Description: A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypotheses	fpr.1	$$⊢A\in \mathrm{V}$$
	fpr.2	$$⊢B\in \mathrm{V}$$
	fpr.3	$$⊢C\in \mathrm{V}$$
	fpr.4	$$⊢D\in \mathrm{V}$$
Assertion	fpr	$$⊢A\ne B\to \left\{⟨A,C⟩,⟨B,D⟩\right\}:\left\{A,B\right\}⟶\left\{C,D\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fpr.1	$$⊢A\in \mathrm{V}$$
2		fpr.2	$$⊢B\in \mathrm{V}$$
3		fpr.3	$$⊢C\in \mathrm{V}$$
4		fpr.4	$$⊢D\in \mathrm{V}$$
5	1 2 3 4	funpr	$$⊢A\ne B\to \mathrm{Fun}\left\{⟨A,C⟩,⟨B,D⟩\right\}$$
6	3 4	dmprop	$$⊢\mathrm{dom}\left\{⟨A,C⟩,⟨B,D⟩\right\}=\left\{A,B\right\}$$
7		df-fn	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}Fn\left\{A,B\right\}\leftrightarrow \left(\mathrm{Fun}\left\{⟨A,C⟩,⟨B,D⟩\right\}\wedge \mathrm{dom}\left\{⟨A,C⟩,⟨B,D⟩\right\}=\left\{A,B\right\}\right)$$
8	5 6 7	sylanblrc	$$⊢A\ne B\to \left\{⟨A,C⟩,⟨B,D⟩\right\}Fn\left\{A,B\right\}$$
9		df-pr	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}=\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}$$
10	9	rneqi	$$⊢\mathrm{ran}\left\{⟨A,C⟩,⟨B,D⟩\right\}=\mathrm{ran}\left(\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}\right)$$
11		rnun	$$⊢\mathrm{ran}\left(\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}\right)=\mathrm{ran}\left\{⟨A,C⟩\right\}\cup \mathrm{ran}\left\{⟨B,D⟩\right\}$$
12	1	rnsnop	$$⊢\mathrm{ran}\left\{⟨A,C⟩\right\}=\left\{C\right\}$$
13	2	rnsnop	$$⊢\mathrm{ran}\left\{⟨B,D⟩\right\}=\left\{D\right\}$$
14	12 13	uneq12i	$$⊢\mathrm{ran}\left\{⟨A,C⟩\right\}\cup \mathrm{ran}\left\{⟨B,D⟩\right\}=\left\{C\right\}\cup \left\{D\right\}$$
15		df-pr	$$⊢\left\{C,D\right\}=\left\{C\right\}\cup \left\{D\right\}$$
16	14 15	eqtr4i	$$⊢\mathrm{ran}\left\{⟨A,C⟩\right\}\cup \mathrm{ran}\left\{⟨B,D⟩\right\}=\left\{C,D\right\}$$
17	10 11 16	3eqtri	$$⊢\mathrm{ran}\left\{⟨A,C⟩,⟨B,D⟩\right\}=\left\{C,D\right\}$$
18	17	eqimssi	$$⊢\mathrm{ran}\left\{⟨A,C⟩,⟨B,D⟩\right\}\subseteq \left\{C,D\right\}$$
19		df-f	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}:\left\{A,B\right\}⟶\left\{C,D\right\}\leftrightarrow \left(\left\{⟨A,C⟩,⟨B,D⟩\right\}Fn\left\{A,B\right\}\wedge \mathrm{ran}\left\{⟨A,C⟩,⟨B,D⟩\right\}\subseteq \left\{C,D\right\}\right)$$
20	8 18 19	sylanblrc	$$⊢A\ne B\to \left\{⟨A,C⟩,⟨B,D⟩\right\}:\left\{A,B\right\}⟶\left\{C,D\right\}$$