fntp

Description: A function with a domain of three elements. (Contributed by NM, 14-Sep-2011) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	fntp.1	$⊢ A \in V$
	fntp.2	$⊢ B \in V$
	fntp.3	$⊢ C \in V$
	fntp.4	$⊢ D \in V$
	fntp.5	$⊢ E \in V$
	fntp.6	$⊢ F \in V$
Assertion	fntp	$⊢ (A \neq B \land A \neq C \land B \neq C) \to \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} Fn \{A, B, C\}$

Step	Hyp	Ref	Expression
1		fntp.1	$⊢ A \in V$
2		fntp.2	$⊢ B \in V$
3		fntp.3	$⊢ C \in V$
4		fntp.4	$⊢ D \in V$
5		fntp.5	$⊢ E \in V$
6		fntp.6	$⊢ F \in V$
7	1 2 3 4 5 6	funtp	$⊢ (A \neq B \land A \neq C \land B \neq C) \to Fun \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\}$
8	4 5 6	dmtpop	$⊢ dom \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} = \{A, B, C\}$
9		df-fn	$⊢ \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} Fn \{A, B, C\} \leftrightarrow (Fun \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} \land dom \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} = \{A, B, C\})$
10	7 8 9	sylanblrc	$⊢ (A \neq B \land A \neq C \land B \neq C) \to \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} Fn \{A, B, C\}$

Metamath Proof Explorer