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 
|- ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
f1dom3fv3dif.n 
|- ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )
f1dom3fv3dif.f 
|- ( ph -> F : { A , B , C } -1-1-> R )
Assertion f1dom3fv3dif 
|- ( ph -> ( ( F ` A ) =/= ( F ` B ) /\ ( F ` A ) =/= ( F ` C ) /\ ( F ` B ) =/= ( F ` C ) ) )

Proof

Step Hyp Ref Expression
1 f1dom3fv3dif.v 
 |-  ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
2 f1dom3fv3dif.n 
 |-  ( ph -> ( A =/= B /\ A =/= C /\ B =/= C ) )
3 f1dom3fv3dif.f 
 |-  ( ph -> F : { A , B , C } -1-1-> R )
4 2 simp1d 
 |-  ( ph -> A =/= B )
5 eqidd 
 |-  ( ph -> A = A )
6 5 3mix1d 
 |-  ( ph -> ( A = A \/ A = B \/ A = C ) )
7 1 simp1d 
 |-  ( ph -> A e. X )
8 eltpg 
 |-  ( A e. X -> ( A e. { A , B , C } <-> ( A = A \/ A = B \/ A = C ) ) )
9 7 8 syl 
 |-  ( ph -> ( A e. { A , B , C } <-> ( A = A \/ A = B \/ A = C ) ) )
10 6 9 mpbird 
 |-  ( ph -> A e. { A , B , C } )
11 eqidd 
 |-  ( ph -> B = B )
12 11 3mix2d 
 |-  ( ph -> ( B = A \/ B = B \/ B = C ) )
13 1 simp2d 
 |-  ( ph -> B e. Y )
14 eltpg 
 |-  ( B e. Y -> ( B e. { A , B , C } <-> ( B = A \/ B = B \/ B = C ) ) )
15 13 14 syl 
 |-  ( ph -> ( B e. { A , B , C } <-> ( B = A \/ B = B \/ B = C ) ) )
16 12 15 mpbird 
 |-  ( ph -> B e. { A , B , C } )
17 f1fveq 
 |-  ( ( F : { A , B , C } -1-1-> R /\ ( A e. { A , B , C } /\ B e. { A , B , C } ) ) -> ( ( F ` A ) = ( F ` B ) <-> A = B ) )
18 3 10 16 17 syl12anc 
 |-  ( ph -> ( ( F ` A ) = ( F ` B ) <-> A = B ) )
19 18 necon3bid 
 |-  ( ph -> ( ( F ` A ) =/= ( F ` B ) <-> A =/= B ) )
20 4 19 mpbird 
 |-  ( ph -> ( F ` A ) =/= ( F ` B ) )
21 2 simp2d 
 |-  ( ph -> A =/= C )
22 1 simp3d 
 |-  ( ph -> C e. Z )
23 tpid3g 
 |-  ( C e. Z -> C e. { A , B , C } )
24 22 23 syl 
 |-  ( ph -> C e. { A , B , C } )
25 f1fveq 
 |-  ( ( F : { A , B , C } -1-1-> R /\ ( A e. { A , B , C } /\ C e. { A , B , C } ) ) -> ( ( F ` A ) = ( F ` C ) <-> A = C ) )
26 3 10 24 25 syl12anc 
 |-  ( ph -> ( ( F ` A ) = ( F ` C ) <-> A = C ) )
27 26 necon3bid 
 |-  ( ph -> ( ( F ` A ) =/= ( F ` C ) <-> A =/= C ) )
28 21 27 mpbird 
 |-  ( ph -> ( F ` A ) =/= ( F ` C ) )
29 2 simp3d 
 |-  ( ph -> B =/= C )
30 f1fveq 
 |-  ( ( F : { A , B , C } -1-1-> R /\ ( B e. { A , B , C } /\ C e. { A , B , C } ) ) -> ( ( F ` B ) = ( F ` C ) <-> B = C ) )
31 3 16 24 30 syl12anc 
 |-  ( ph -> ( ( F ` B ) = ( F ` C ) <-> B = C ) )
32 31 necon3bid 
 |-  ( ph -> ( ( F ` B ) =/= ( F ` C ) <-> B =/= C ) )
33 29 32 mpbird 
 |-  ( ph -> ( F ` B ) =/= ( F ` C ) )
34 20 28 33 3jca 
 |-  ( ph -> ( ( F ` A ) =/= ( F ` B ) /\ ( F ` A ) =/= ( F ` C ) /\ ( F ` B ) =/= ( F ` C ) ) )