Theorem 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 \mathrm{V}$$
	fntp.2	$$⊢B\in \mathrm{V}$$
	fntp.3	$$⊢C\in \mathrm{V}$$
	fntp.4	$$⊢D\in \mathrm{V}$$
	fntp.5	$$⊢E\in \mathrm{V}$$
	fntp.6	$$⊢F\in \mathrm{V}$$
Assertion	fntp	$$⊢\left(A\ne B\wedge A\ne C\wedge B\ne C\right)\to \left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}Fn\left\{A,B,C\right\}$$

Proof

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