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 ⊢ A = 0 … 2
Assertion f13idfv ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ F ⁡ 0 ≠ F ⁡ 1 ∧ F ⁡ 0 ≠ F ⁡ 2 ∧ F ⁡ 1 ≠ F ⁡ 2

Proof

Step Hyp Ref Expression
1 f13idfv.a ⊢ 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 ⊢ A = 0 1 2
12 11 f13dfv ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 0 ≠ 1 ∧ 0 ≠ 2 ∧ 1 ≠ 2 → F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ F ⁡ 0 ≠ F ⁡ 1 ∧ F ⁡ 0 ≠ F ⁡ 2 ∧ F ⁡ 1 ≠ F ⁡ 2
13 5 9 12 mp2an ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ F ⁡ 0 ≠ F ⁡ 1 ∧ F ⁡ 0 ≠ F ⁡ 2 ∧ F ⁡ 1 ≠ F ⁡ 2