This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )