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)

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

Metamath Proof Explorer