Metamath Proof Explorer

Theorem s3f1

Description: Conditions for a length 3 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses s3f1.i 
|- ( ph -> I e. D )
s3f1.j 
|- ( ph -> J e. D )
s3f1.k 
|- ( ph -> K e. D )
s3f1.1 
|- ( ph -> I =/= J )
s3f1.2 
|- ( ph -> J =/= K )
s3f1.3 
|- ( ph -> K =/= I )
Assertion s3f1 
|- ( ph -> <" I J K "> : dom <" I J K "> -1-1-> D )

Proof

Step Hyp Ref Expression
1 s3f1.i 
 |-  ( ph -> I e. D )
2 s3f1.j 
 |-  ( ph -> J e. D )
3 s3f1.k 
 |-  ( ph -> K e. D )
4 s3f1.1 
 |-  ( ph -> I =/= J )
5 s3f1.2 
 |-  ( ph -> J =/= K )
6 s3f1.3 
 |-  ( ph -> K =/= I )
7 1 2 3 s3cld 
 |-  ( ph -> <" I J K "> e. Word D )
8 wrdf 
 |-  ( <" I J K "> e. Word D -> <" I J K "> : ( 0 ..^ ( # ` <" I J K "> ) ) --> D )
9 7 8 syl 
 |-  ( ph -> <" I J K "> : ( 0 ..^ ( # ` <" I J K "> ) ) --> D )
10 9 ffdmd 
 |-  ( ph -> <" I J K "> : dom <" I J K "> --> D )
11 simplr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 0 ) -> i = 0 )
12 simpr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 0 ) -> j = 0 )
13 11 12 eqtr4d 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 0 ) -> i = j )
14 simpllr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 1 ) -> ( <" I J K "> ` i ) = ( <" I J K "> ` j ) )
15 simpr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) -> i = 0 )
16 15 fveq2d 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) -> ( <" I J K "> ` i ) = ( <" I J K "> ` 0 ) )
17 s3fv0 
 |-  ( I e. D -> ( <" I J K "> ` 0 ) = I )
18 1 17 syl 
 |-  ( ph -> ( <" I J K "> ` 0 ) = I )
19 18 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) -> ( <" I J K "> ` 0 ) = I )
20 16 19 eqtrd 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) -> ( <" I J K "> ` i ) = I )
21 20 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 1 ) -> ( <" I J K "> ` i ) = I )
22 simpr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 1 ) -> j = 1 )
23 22 fveq2d 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 1 ) -> ( <" I J K "> ` j ) = ( <" I J K "> ` 1 ) )
24 s3fv1 
 |-  ( J e. D -> ( <" I J K "> ` 1 ) = J )
25 2 24 syl 
 |-  ( ph -> ( <" I J K "> ` 1 ) = J )
26 25 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 1 ) -> ( <" I J K "> ` 1 ) = J )
27 23 26 eqtrd 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 1 ) -> ( <" I J K "> ` j ) = J )
28 27 adantlr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 1 ) -> ( <" I J K "> ` j ) = J )
29 14 21 28 3eqtr3d 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 1 ) -> I = J )
30 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 1 ) -> I =/= J )
31 29 30 pm2.21ddne 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 1 ) -> i = j )
32 simpllr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 2 ) -> ( <" I J K "> ` i ) = ( <" I J K "> ` j ) )
33 20 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 2 ) -> ( <" I J K "> ` i ) = I )
34 simpr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 2 ) -> j = 2 )
35 34 fveq2d 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 2 ) -> ( <" I J K "> ` j ) = ( <" I J K "> ` 2 ) )
36 s3fv2 
 |-  ( K e. D -> ( <" I J K "> ` 2 ) = K )
37 3 36 syl 
 |-  ( ph -> ( <" I J K "> ` 2 ) = K )
38 37 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 2 ) -> ( <" I J K "> ` 2 ) = K )
39 35 38 eqtrd 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 2 ) -> ( <" I J K "> ` j ) = K )
40 39 adantlr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 2 ) -> ( <" I J K "> ` j ) = K )
41 32 33 40 3eqtr3rd 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 2 ) -> K = I )
42 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 2 ) -> K =/= I )
43 41 42 pm2.21ddne 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) /\ j = 2 ) -> i = j )
44 wrddm 
 |-  ( <" I J K "> e. Word D -> dom <" I J K "> = ( 0 ..^ ( # ` <" I J K "> ) ) )
45 7 44 syl 
 |-  ( ph -> dom <" I J K "> = ( 0 ..^ ( # ` <" I J K "> ) ) )
46 s3len 
 |-  ( # ` <" I J K "> ) = 3
47 46 oveq2i 
 |-  ( 0 ..^ ( # ` <" I J K "> ) ) = ( 0 ..^ 3 )
48 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
49 47 48 eqtri 
 |-  ( 0 ..^ ( # ` <" I J K "> ) ) = { 0 , 1 , 2 }
50 45 49 eqtrdi 
 |-  ( ph -> dom <" I J K "> = { 0 , 1 , 2 } )
51 50 eleq2d 
 |-  ( ph -> ( j e. dom <" I J K "> <-> j e. { 0 , 1 , 2 } ) )
52 51 biimpa 
 |-  ( ( ph /\ j e. dom <" I J K "> ) -> j e. { 0 , 1 , 2 } )
53 vex 
 |-  j e. _V
54 53 eltp 
 |-  ( j e. { 0 , 1 , 2 } <-> ( j = 0 \/ j = 1 \/ j = 2 ) )
55 52 54 sylib 
 |-  ( ( ph /\ j e. dom <" I J K "> ) -> ( j = 0 \/ j = 1 \/ j = 2 ) )
56 55 adantlr 
 |-  ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) -> ( j = 0 \/ j = 1 \/ j = 2 ) )
57 56 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) -> ( j = 0 \/ j = 1 \/ j = 2 ) )
58 13 31 43 57 mpjao3dan 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 0 ) -> i = j )
59 simpllr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 0 ) -> ( <" I J K "> ` i ) = ( <" I J K "> ` j ) )
60 simpr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) -> i = 1 )
61 60 fveq2d 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) -> ( <" I J K "> ` i ) = ( <" I J K "> ` 1 ) )
62 25 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) -> ( <" I J K "> ` 1 ) = J )
63 61 62 eqtrd 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) -> ( <" I J K "> ` i ) = J )
64 63 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 0 ) -> ( <" I J K "> ` i ) = J )
65 simpr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 0 ) -> j = 0 )
66 65 fveq2d 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 0 ) -> ( <" I J K "> ` j ) = ( <" I J K "> ` 0 ) )
67 18 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 0 ) -> ( <" I J K "> ` 0 ) = I )
68 66 67 eqtrd 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ j = 0 ) -> ( <" I J K "> ` j ) = I )
69 68 adantlr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 0 ) -> ( <" I J K "> ` j ) = I )
70 59 64 69 3eqtr3rd 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 0 ) -> I = J )
71 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 0 ) -> I =/= J )
72 70 71 pm2.21ddne 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 0 ) -> i = j )
73 simplr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 1 ) -> i = 1 )
74 simpr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 1 ) -> j = 1 )
75 73 74 eqtr4d 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 1 ) -> i = j )
76 simpllr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 2 ) -> ( <" I J K "> ` i ) = ( <" I J K "> ` j ) )
77 63 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 2 ) -> ( <" I J K "> ` i ) = J )
78 39 adantlr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 2 ) -> ( <" I J K "> ` j ) = K )
79 76 77 78 3eqtr3d 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 2 ) -> J = K )
80 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 2 ) -> J =/= K )
81 79 80 pm2.21ddne 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) /\ j = 2 ) -> i = j )
82 56 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) -> ( j = 0 \/ j = 1 \/ j = 2 ) )
83 72 75 81 82 mpjao3dan 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 1 ) -> i = j )
84 simpllr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 0 ) -> ( <" I J K "> ` i ) = ( <" I J K "> ` j ) )
85 simpr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) -> i = 2 )
86 85 fveq2d 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) -> ( <" I J K "> ` i ) = ( <" I J K "> ` 2 ) )
87 37 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) -> ( <" I J K "> ` 2 ) = K )
88 86 87 eqtrd 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) -> ( <" I J K "> ` i ) = K )
89 88 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 0 ) -> ( <" I J K "> ` i ) = K )
90 68 adantlr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 0 ) -> ( <" I J K "> ` j ) = I )
91 84 89 90 3eqtr3d 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 0 ) -> K = I )
92 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 0 ) -> K =/= I )
93 91 92 pm2.21ddne 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 0 ) -> i = j )
94 simpllr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 1 ) -> ( <" I J K "> ` i ) = ( <" I J K "> ` j ) )
95 88 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 1 ) -> ( <" I J K "> ` i ) = K )
96 27 adantlr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 1 ) -> ( <" I J K "> ` j ) = J )
97 94 95 96 3eqtr3rd 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 1 ) -> J = K )
98 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 1 ) -> J =/= K )
99 97 98 pm2.21ddne 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 1 ) -> i = j )
100 simplr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 2 ) -> i = 2 )
101 simpr 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 2 ) -> j = 2 )
102 100 101 eqtr4d 
 |-  ( ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) /\ j = 2 ) -> i = j )
103 56 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) -> ( j = 0 \/ j = 1 \/ j = 2 ) )
104 93 99 102 103 mpjao3dan 
 |-  ( ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) /\ i = 2 ) -> i = j )
105 50 eleq2d 
 |-  ( ph -> ( i e. dom <" I J K "> <-> i e. { 0 , 1 , 2 } ) )
106 105 biimpa 
 |-  ( ( ph /\ i e. dom <" I J K "> ) -> i e. { 0 , 1 , 2 } )
107 vex 
 |-  i e. _V
108 107 eltp 
 |-  ( i e. { 0 , 1 , 2 } <-> ( i = 0 \/ i = 1 \/ i = 2 ) )
109 106 108 sylib 
 |-  ( ( ph /\ i e. dom <" I J K "> ) -> ( i = 0 \/ i = 1 \/ i = 2 ) )
110 109 ad2antrr 
 |-  ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) -> ( i = 0 \/ i = 1 \/ i = 2 ) )
111 58 83 104 110 mpjao3dan 
 |-  ( ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) /\ ( <" I J K "> ` i ) = ( <" I J K "> ` j ) ) -> i = j )
112 111 ex 
 |-  ( ( ( ph /\ i e. dom <" I J K "> ) /\ j e. dom <" I J K "> ) -> ( ( <" I J K "> ` i ) = ( <" I J K "> ` j ) -> i = j ) )
113 112 anasss 
 |-  ( ( ph /\ ( i e. dom <" I J K "> /\ j e. dom <" I J K "> ) ) -> ( ( <" I J K "> ` i ) = ( <" I J K "> ` j ) -> i = j ) )
114 113 ralrimivva 
 |-  ( ph -> A. i e. dom <" I J K "> A. j e. dom <" I J K "> ( ( <" I J K "> ` i ) = ( <" I J K "> ` j ) -> i = j ) )
115 dff13 
 |-  ( <" I J K "> : dom <" I J K "> -1-1-> D <-> ( <" I J K "> : dom <" I J K "> --> D /\ A. i e. dom <" I J K "> A. j e. dom <" I J K "> ( ( <" I J K "> ` i ) = ( <" I J K "> ` j ) -> i = j ) ) )
116 10 114 115 sylanbrc 
 |-  ( ph -> <" I J K "> : dom <" I J K "> -1-1-> D )