Metamath Proof Explorer

Theorem f1dom3fv3dif

Description: The function values for a 1-1 function from a set with three different elements are different. (Contributed by AV, 20-Mar-2019)

Ref Expression
Hypotheses f1dom3fv3dif.v ⊢ φ → A ∈ X ∧ B ∈ Y ∧ C ∈ Z
f1dom3fv3dif.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C
f1dom3fv3dif.f ⊢ φ → F : A B C ⟶ 1-1 R
Assertion f1dom3fv3dif ⊢ φ → F ⁡ A ≠ F ⁡ B ∧ F ⁡ A ≠ F ⁡ C ∧ F ⁡ B ≠ F ⁡ C

Proof

Step Hyp Ref Expression
1 f1dom3fv3dif.v ⊢ φ → A ∈ X ∧ B ∈ Y ∧ C ∈ Z
2 f1dom3fv3dif.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C
3 f1dom3fv3dif.f ⊢ φ → F : A B C ⟶ 1-1 R
4 2 simp1d ⊢ φ → A ≠ B
5 eqidd ⊢ φ → A = A
6 5 3mix1d ⊢ φ → A = A ∨ A = B ∨ A = C
7 1 simp1d ⊢ φ → A ∈ X
8 eltpg ⊢ A ∈ X → A ∈ A B C ↔ A = A ∨ A = B ∨ A = C
9 7 8 syl ⊢ φ → A ∈ A B C ↔ A = A ∨ A = B ∨ A = C
10 6 9 mpbird ⊢ φ → A ∈ A B C
11 eqidd ⊢ φ → B = B
12 11 3mix2d ⊢ φ → B = A ∨ B = B ∨ B = C
13 1 simp2d ⊢ φ → B ∈ Y
14 eltpg ⊢ B ∈ Y → B ∈ A B C ↔ B = A ∨ B = B ∨ B = C
15 13 14 syl ⊢ φ → B ∈ A B C ↔ B = A ∨ B = B ∨ B = C
16 12 15 mpbird ⊢ φ → B ∈ A B C
17 f1fveq ⊢ F : A B C ⟶ 1-1 R ∧ A ∈ A B C ∧ B ∈ A B C → F ⁡ A = F ⁡ B ↔ A = B
18 3 10 16 17 syl12anc ⊢ φ → F ⁡ A = F ⁡ B ↔ A = B
19 18 necon3bid ⊢ φ → F ⁡ A ≠ F ⁡ B ↔ A ≠ B
20 4 19 mpbird ⊢ φ → F ⁡ A ≠ F ⁡ B
21 2 simp2d ⊢ φ → A ≠ C
22 1 simp3d ⊢ φ → C ∈ Z
23 tpid3g ⊢ C ∈ Z → C ∈ A B C
24 22 23 syl ⊢ φ → C ∈ A B C
25 f1fveq ⊢ F : A B C ⟶ 1-1 R ∧ A ∈ A B C ∧ C ∈ A B C → F ⁡ A = F ⁡ C ↔ A = C
26 3 10 24 25 syl12anc ⊢ φ → F ⁡ A = F ⁡ C ↔ A = C
27 26 necon3bid ⊢ φ → F ⁡ A ≠ F ⁡ C ↔ A ≠ C
28 21 27 mpbird ⊢ φ → F ⁡ A ≠ F ⁡ C
29 2 simp3d ⊢ φ → B ≠ C
30 f1fveq ⊢ F : A B C ⟶ 1-1 R ∧ B ∈ A B C ∧ C ∈ A B C → F ⁡ B = F ⁡ C ↔ B = C
31 3 16 24 30 syl12anc ⊢ φ → F ⁡ B = F ⁡ C ↔ B = C
32 31 necon3bid ⊢ φ → F ⁡ B ≠ F ⁡ C ↔ B ≠ C
33 29 32 mpbird ⊢ φ → F ⁡ B ≠ F ⁡ C
34 20 28 33 3jca ⊢ φ → F ⁡ A ≠ F ⁡ B ∧ F ⁡ A ≠ F ⁡ C ∧ F ⁡ B ≠ F ⁡ C