Metamath Proof Explorer

Theorem f1dom3el3dif

Description: The codomain of a 1-1 function from a set with three different elements has (at least) three different elements. (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 f1dom3el3dif 
|- ( ph -> E. x e. R E. y e. R E. z e. R ( x =/= y /\ x =/= z /\ y =/= z ) )

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 f1f 
 |-  ( F : { A , B , C } -1-1-> R -> F : { A , B , C } --> R )
5 simpr 
 |-  ( ( ph /\ F : { A , B , C } --> R ) -> F : { A , B , C } --> R )
6 eqidd 
 |-  ( ph -> A = A )
7 6 3mix1d 
 |-  ( ph -> ( A = A \/ A = B \/ A = C ) )
8 1 simp1d 
 |-  ( ph -> A e. X )
9 eltpg 
 |-  ( A e. X -> ( A e. { A , B , C } <-> ( A = A \/ A = B \/ A = C ) ) )
10 8 9 syl 
 |-  ( ph -> ( A e. { A , B , C } <-> ( A = A \/ A = B \/ A = C ) ) )
11 7 10 mpbird 
 |-  ( ph -> A e. { A , B , C } )
12 11 adantr 
 |-  ( ( ph /\ F : { A , B , C } --> R ) -> A e. { A , B , C } )
13 5 12 ffvelcdmd 
 |-  ( ( ph /\ F : { A , B , C } --> R ) -> ( F ` A ) e. R )
14 eqidd 
 |-  ( ph -> B = B )
15 14 3mix2d 
 |-  ( ph -> ( B = A \/ B = B \/ B = C ) )
16 1 simp2d 
 |-  ( ph -> B e. Y )
17 eltpg 
 |-  ( B e. Y -> ( B e. { A , B , C } <-> ( B = A \/ B = B \/ B = C ) ) )
18 16 17 syl 
 |-  ( ph -> ( B e. { A , B , C } <-> ( B = A \/ B = B \/ B = C ) ) )
19 15 18 mpbird 
 |-  ( ph -> B e. { A , B , C } )
20 19 adantr 
 |-  ( ( ph /\ F : { A , B , C } --> R ) -> B e. { A , B , C } )
21 5 20 ffvelcdmd 
 |-  ( ( ph /\ F : { A , B , C } --> R ) -> ( F ` B ) e. R )
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 24 adantr 
 |-  ( ( ph /\ F : { A , B , C } --> R ) -> C e. { A , B , C } )
26 5 25 ffvelcdmd 
 |-  ( ( ph /\ F : { A , B , C } --> R ) -> ( F ` C ) e. R )
27 13 21 26 3jca 
 |-  ( ( ph /\ F : { A , B , C } --> R ) -> ( ( F ` A ) e. R /\ ( F ` B ) e. R /\ ( F ` C ) e. R ) )
28 27 expcom 
 |-  ( F : { A , B , C } --> R -> ( ph -> ( ( F ` A ) e. R /\ ( F ` B ) e. R /\ ( F ` C ) e. R ) ) )
29 4 28 syl 
 |-  ( F : { A , B , C } -1-1-> R -> ( ph -> ( ( F ` A ) e. R /\ ( F ` B ) e. R /\ ( F ` C ) e. R ) ) )
30 3 29 mpcom 
 |-  ( ph -> ( ( F ` A ) e. R /\ ( F ` B ) e. R /\ ( F ` C ) e. R ) )
31 1 2 3 f1dom3fv3dif 
 |-  ( ph -> ( ( F ` A ) =/= ( F ` B ) /\ ( F ` A ) =/= ( F ` C ) /\ ( F ` B ) =/= ( F ` C ) ) )
32 neeq1 
 |-  ( x = ( F ` A ) -> ( x =/= y <-> ( F ` A ) =/= y ) )
33 neeq1 
 |-  ( x = ( F ` A ) -> ( x =/= z <-> ( F ` A ) =/= z ) )
34 32 33 3anbi12d 
 |-  ( x = ( F ` A ) -> ( ( x =/= y /\ x =/= z /\ y =/= z ) <-> ( ( F ` A ) =/= y /\ ( F ` A ) =/= z /\ y =/= z ) ) )
35 neeq2 
 |-  ( y = ( F ` B ) -> ( ( F ` A ) =/= y <-> ( F ` A ) =/= ( F ` B ) ) )
36 neeq1 
 |-  ( y = ( F ` B ) -> ( y =/= z <-> ( F ` B ) =/= z ) )
37 35 36 3anbi13d 
 |-  ( y = ( F ` B ) -> ( ( ( F ` A ) =/= y /\ ( F ` A ) =/= z /\ y =/= z ) <-> ( ( F ` A ) =/= ( F ` B ) /\ ( F ` A ) =/= z /\ ( F ` B ) =/= z ) ) )
38 neeq2 
 |-  ( z = ( F ` C ) -> ( ( F ` A ) =/= z <-> ( F ` A ) =/= ( F ` C ) ) )
39 neeq2 
 |-  ( z = ( F ` C ) -> ( ( F ` B ) =/= z <-> ( F ` B ) =/= ( F ` C ) ) )
40 38 39 3anbi23d 
 |-  ( z = ( F ` C ) -> ( ( ( F ` A ) =/= ( F ` B ) /\ ( F ` A ) =/= z /\ ( F ` B ) =/= z ) <-> ( ( F ` A ) =/= ( F ` B ) /\ ( F ` A ) =/= ( F ` C ) /\ ( F ` B ) =/= ( F ` C ) ) ) )
41 34 37 40 rspc3ev 
 |-  ( ( ( ( F ` A ) e. R /\ ( F ` B ) e. R /\ ( F ` C ) e. R ) /\ ( ( F ` A ) =/= ( F ` B ) /\ ( F ` A ) =/= ( F ` C ) /\ ( F ` B ) =/= ( F ` C ) ) ) -> E. x e. R E. y e. R E. z e. R ( x =/= y /\ x =/= z /\ y =/= z ) )
42 30 31 41 syl2anc 
 |-  ( ph -> E. x e. R E. y e. R E. z e. R ( x =/= y /\ x =/= z /\ y =/= z ) )