# 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 ( 𝜑 → ( ( 𝐹𝐴 ) ≠ ( 𝐹𝐵 ) ∧ ( 𝐹𝐴 ) ≠ ( 𝐹𝐶 ) ∧ ( 𝐹𝐵 ) ≠ ( 𝐹𝐶 ) ) )