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

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 ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
f1dom3fv3dif.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) )
f1dom3fv3dif.f ⊢ ( 𝜑 → 𝐹 : { 𝐴 , 𝐵 , 𝐶 } –1-1→ 𝑅 )
Assertion f1dom3fv3dif ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) ≠ ( 𝐹 ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 f1dom3fv3dif.v ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
2 f1dom3fv3dif.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) )
3 f1dom3fv3dif.f ⊢ ( 𝜑 → 𝐹 : { 𝐴 , 𝐵 , 𝐶 } –1-1→ 𝑅 )
4 2 simp1d ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
5 eqidd ⊢ ( 𝜑 → 𝐴 = 𝐴 )
6 5 3mix1d ⊢ ( 𝜑 → ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )
7 1 simp1d ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 eltpg ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
9 7 8 syl ⊢ ( 𝜑 → ( 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
10 6 9 mpbird ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } )
11 eqidd ⊢ ( 𝜑 → 𝐵 = 𝐵 )
12 11 3mix2d ⊢ ( 𝜑 → ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶 ) )
13 1 simp2d ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
14 eltpg ⊢ ( 𝐵 ∈ 𝑌 → ( 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶 ) ) )
15 13 14 syl ⊢ ( 𝜑 → ( 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶 ) ) )
16 12 15 mpbird ⊢ ( 𝜑 → 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } )
17 f1fveq ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 , 𝐶 } –1-1→ 𝑅 ∧ ( 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )
18 3 10 16 17 syl12anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )
19 18 necon3bid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐵 ) ↔ 𝐴 ≠ 𝐵 ) )
20 4 19 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐵 ) )
21 2 simp2d ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
22 1 simp3d ⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
23 tpid3g ⊢ ( 𝐶 ∈ 𝑍 → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
24 22 23 syl ⊢ ( 𝜑 → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
25 f1fveq ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 , 𝐶 } –1-1→ 𝑅 ∧ ( 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐴 = 𝐶 ) )
26 3 10 24 25 syl12anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐴 = 𝐶 ) )
27 26 necon3bid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐶 ) ↔ 𝐴 ≠ 𝐶 ) )
28 21 27 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐶 ) )
29 2 simp3d ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
30 f1fveq ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 , 𝐶 } –1-1→ 𝑅 ∧ ( 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐵 = 𝐶 ) )
31 3 16 24 30 syl12anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐵 = 𝐶 ) )
32 31 necon3bid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ≠ ( 𝐹 ‘ 𝐶 ) ↔ 𝐵 ≠ 𝐶 ) )
33 29 32 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ≠ ( 𝐹 ‘ 𝐶 ) )
34 20 28 33 3jca ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) ≠ ( 𝐹 ‘ 𝐶 ) ) )