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	⊢ 𝐴 = ( 0 ... 2 )
Assertion	f13idfv	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 2 ) ∧ ( 𝐹 ‘ 1 ) ≠ ( 𝐹 ‘ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		f13idfv.a	⊢ 𝐴 = ( 0 ... 2 )
2		0z	⊢ 0 ∈ ℤ
3		1z	⊢ 1 ∈ ℤ
4		2z	⊢ 2 ∈ ℤ
5	2 3 4	3pm3.2i	⊢ ( 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ )
6		0ne1	⊢ 0 ≠ 1
7		0ne2	⊢ 0 ≠ 2
8		1ne2	⊢ 1 ≠ 2
9	6 7 8	3pm3.2i	⊢ ( 0 ≠ 1 ∧ 0 ≠ 2 ∧ 1 ≠ 2 )
10		fz0tp	⊢ ( 0 ... 2 ) = { 0 , 1 , 2 }
11	1 10	eqtri	⊢ 𝐴 = { 0 , 1 , 2 }
12	11	f13dfv	⊢ ( ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 0 ≠ 1 ∧ 0 ≠ 2 ∧ 1 ≠ 2 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 2 ) ∧ ( 𝐹 ‘ 1 ) ≠ ( 𝐹 ‘ 2 ) ) ) ) )
13	5 9 12	mp2an	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 2 ) ∧ ( 𝐹 ‘ 1 ) ≠ ( 𝐹 ‘ 2 ) ) ) )