Theorem f13idfv

Description: A one-to-one function with the domain { 0, 1 ,2 } in terms of function values. (Contributed by Alexander van der Vekens, 26-Jan-2018)

	Ref	Expression
Hypothesis	f13idfv.a	$$⊢A=\left(0\dots 2\right)$$
Assertion	f13idfv	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \left(F\left(0\right)\ne F\left(1\right)\wedge F\left(0\right)\ne F\left(2\right)\wedge F\left(1\right)\ne F\left(2\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		f13idfv.a	$$⊢A=\left(0\dots 2\right)$$
2		0z	$$⊢0\in \mathbb{Z}$$
3		1z	$$⊢1\in \mathbb{Z}$$
4		2z	$$⊢2\in \mathbb{Z}$$
5	2 3 4	3pm3.2i	$$⊢\left(0\in \mathbb{Z}\wedge 1\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)$$
6		0ne1	$$⊢0\ne 1$$
7		0ne2	$$⊢0\ne 2$$
8		1ne2	$$⊢1\ne 2$$
9	6 7 8	3pm3.2i	$$⊢\left(0\ne 1\wedge 0\ne 2\wedge 1\ne 2\right)$$
10		fz0tp	$$⊢\left(0\dots 2\right)=\left\{0,1,2\right\}$$
11	1 10	eqtri	$$⊢A=\left\{0,1,2\right\}$$
12	11	f13dfv	$$⊢\left(\left(0\in \mathbb{Z}\wedge 1\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\wedge \left(0\ne 1\wedge 0\ne 2\wedge 1\ne 2\right)\right)\to \left(F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \left(F\left(0\right)\ne F\left(1\right)\wedge F\left(0\right)\ne F\left(2\right)\wedge F\left(1\right)\ne F\left(2\right)\right)\right)\right)$$
13	5 9 12	mp2an	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \left(F\left(0\right)\ne F\left(1\right)\wedge F\left(0\right)\ne F\left(2\right)\wedge F\left(1\right)\ne F\left(2\right)\right)\right)$$