# Metamath Proof Explorer

## 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\}↔\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\}↔\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\}$