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

Metamath Proof Explorer

Theorem efgredlem

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
efgred.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
efgred.s 
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
efgredlem.1 
|- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
efgredlem.2 
|- ( ph -> A e. dom S )
efgredlem.3 
|- ( ph -> B e. dom S )
efgredlem.4 
|- ( ph -> ( S ` A ) = ( S ` B ) )
efgredlem.5 
|- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )
Assertion efgredlem 
|- -. ph

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 efgval2.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 efgred.d 
 |-  D = ( W \ U_ x e. W ran ( T ` x ) )
6 efgred.s 
 |-  S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
7 efgredlem.1 
 |-  ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
8 efgredlem.2 
 |-  ( ph -> A e. dom S )
9 efgredlem.3 
 |-  ( ph -> B e. dom S )
10 efgredlem.4 
 |-  ( ph -> ( S ` A ) = ( S ` B ) )
11 efgredlem.5 
 |-  ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )
12 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
13 1 12 eqsstri 
 |-  W C_ Word ( I X. 2o )
14 1 2 3 4 5 6 efgsdm 
 |-  ( A e. dom S <-> ( A e. ( Word W \ { (/) } ) /\ ( A ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` A ) ) ( A ` i ) e. ran ( T ` ( A ` ( i - 1 ) ) ) ) )
15 14 simp1bi 
 |-  ( A e. dom S -> A e. ( Word W \ { (/) } ) )
16 8 15 syl 
 |-  ( ph -> A e. ( Word W \ { (/) } ) )
17 16 eldifad 
 |-  ( ph -> A e. Word W )
18 wrdf 
 |-  ( A e. Word W -> A : ( 0 ..^ ( # ` A ) ) --> W )
19 17 18 syl 
 |-  ( ph -> A : ( 0 ..^ ( # ` A ) ) --> W )
20 1 2 3 4 5 6 7 8 9 10 11 efgredlema 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )
21 20 simpld 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. NN )
22 nnm1nn0 
 |-  ( ( ( # ` A ) - 1 ) e. NN -> ( ( ( # ` A ) - 1 ) - 1 ) e. NN0 )
23 21 22 syl 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) - 1 ) e. NN0 )
24 21 nnred 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. RR )
25 24 lem1d 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) - 1 ) <_ ( ( # ` A ) - 1 ) )
26 eldifsni 
 |-  ( A e. ( Word W \ { (/) } ) -> A =/= (/) )
27 8 15 26 3syl 
 |-  ( ph -> A =/= (/) )
28 wrdfin 
 |-  ( A e. Word W -> A e. Fin )
29 hashnncl 
 |-  ( A e. Fin -> ( ( # ` A ) e. NN <-> A =/= (/) ) )
30 17 28 29 3syl 
 |-  ( ph -> ( ( # ` A ) e. NN <-> A =/= (/) ) )
31 27 30 mpbird 
 |-  ( ph -> ( # ` A ) e. NN )
32 nnm1nn0 
 |-  ( ( # ` A ) e. NN -> ( ( # ` A ) - 1 ) e. NN0 )
33 fznn0 
 |-  ( ( ( # ` A ) - 1 ) e. NN0 -> ( ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ... ( ( # ` A ) - 1 ) ) <-> ( ( ( ( # ` A ) - 1 ) - 1 ) e. NN0 /\ ( ( ( # ` A ) - 1 ) - 1 ) <_ ( ( # ` A ) - 1 ) ) ) )
34 31 32 33 3syl 
 |-  ( ph -> ( ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ... ( ( # ` A ) - 1 ) ) <-> ( ( ( ( # ` A ) - 1 ) - 1 ) e. NN0 /\ ( ( ( # ` A ) - 1 ) - 1 ) <_ ( ( # ` A ) - 1 ) ) ) )
35 23 25 34 mpbir2and 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ... ( ( # ` A ) - 1 ) ) )
36 lencl 
 |-  ( A e. Word W -> ( # ` A ) e. NN0 )
37 17 36 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
38 37 nn0zd 
 |-  ( ph -> ( # ` A ) e. ZZ )
39 fzoval 
 |-  ( ( # ` A ) e. ZZ -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
40 38 39 syl 
 |-  ( ph -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
41 35 40 eleqtrrd 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( # ` A ) ) )
42 19 41 ffvelcdmd 
 |-  ( ph -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) e. W )
43 13 42 sselid 
 |-  ( ph -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) e. Word ( I X. 2o ) )
44 lencl 
 |-  ( ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) e. Word ( I X. 2o ) -> ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) e. NN0 )
45 43 44 syl 
 |-  ( ph -> ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) e. NN0 )
46 45 nn0red 
 |-  ( ph -> ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) e. RR )
47 2rp 
 |-  2 e. RR+
48 ltaddrp 
 |-  ( ( ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) e. RR /\ 2 e. RR+ ) -> ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) < ( ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) + 2 ) )
49 46 47 48 sylancl 
 |-  ( ph -> ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) < ( ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) + 2 ) )
50 37 nn0red 
 |-  ( ph -> ( # ` A ) e. RR )
51 50 lem1d 
 |-  ( ph -> ( ( # ` A ) - 1 ) <_ ( # ` A ) )
52 fznn 
 |-  ( ( # ` A ) e. ZZ -> ( ( ( # ` A ) - 1 ) e. ( 1 ... ( # ` A ) ) <-> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` A ) - 1 ) <_ ( # ` A ) ) ) )
53 38 52 syl 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) e. ( 1 ... ( # ` A ) ) <-> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` A ) - 1 ) <_ ( # ` A ) ) ) )
54 21 51 53 mpbir2and 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. ( 1 ... ( # ` A ) ) )
55 1 2 3 4 5 6 efgsres 
 |-  ( ( A e. dom S /\ ( ( # ` A ) - 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) e. dom S )
56 8 54 55 syl2anc 
 |-  ( ph -> ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) e. dom S )
57 1 2 3 4 5 6 efgsval 
 |-  ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) e. dom S -> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) - 1 ) ) )
58 56 57 syl 
 |-  ( ph -> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) - 1 ) ) )
59 fz1ssfz0 
 |-  ( 1 ... ( # ` A ) ) C_ ( 0 ... ( # ` A ) )
60 59 54 sselid 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. ( 0 ... ( # ` A ) ) )
61 pfxres 
 |-  ( ( A e. Word W /\ ( ( # ` A ) - 1 ) e. ( 0 ... ( # ` A ) ) ) -> ( A prefix ( ( # ` A ) - 1 ) ) = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) )
62 17 60 61 syl2anc 
 |-  ( ph -> ( A prefix ( ( # ` A ) - 1 ) ) = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) )
63 62 fveq2d 
 |-  ( ph -> ( # ` ( A prefix ( ( # ` A ) - 1 ) ) ) = ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) )
64 pfxlen 
 |-  ( ( A e. Word W /\ ( ( # ` A ) - 1 ) e. ( 0 ... ( # ` A ) ) ) -> ( # ` ( A prefix ( ( # ` A ) - 1 ) ) ) = ( ( # ` A ) - 1 ) )
65 17 60 64 syl2anc 
 |-  ( ph -> ( # ` ( A prefix ( ( # ` A ) - 1 ) ) ) = ( ( # ` A ) - 1 ) )
66 63 65 eqtr3d 
 |-  ( ph -> ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( ( # ` A ) - 1 ) )
67 66 fvoveq1d 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) - 1 ) ) = ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
68 fzo0end 
 |-  ( ( ( # ` A ) - 1 ) e. NN -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
69 fvres 
 |-  ( ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
70 21 68 69 3syl 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
71 58 67 70 3eqtrd 
 |-  ( ph -> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
72 71 fveq2d 
 |-  ( ph -> ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) = ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
73 1 2 3 4 5 6 efgsdmi 
 |-  ( ( A e. dom S /\ ( ( # ` A ) - 1 ) e. NN ) -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
74 8 21 73 syl2anc 
 |-  ( ph -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
75 1 2 3 4 efgtlen 
 |-  ( ( ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) e. W /\ ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) -> ( # ` ( S ` A ) ) = ( ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) + 2 ) )
76 42 74 75 syl2anc 
 |-  ( ph -> ( # ` ( S ` A ) ) = ( ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) + 2 ) )
77 49 72 76 3brtr4d 
 |-  ( ph -> ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) )
78 1 2 3 4 efgtf 
 |-  ( ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) e. W -> ( ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) = ( a e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) , b e. ( I X. 2o ) |-> ( ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) : ( ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) --> W ) )
79 42 78 syl 
 |-  ( ph -> ( ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) = ( a e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) , b e. ( I X. 2o ) |-> ( ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) : ( ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) --> W ) )
80 79 simprd 
 |-  ( ph -> ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) : ( ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) --> W )
81 ffn 
 |-  ( ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) : ( ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) --> W -> ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) Fn ( ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) )
82 ovelrn 
 |-  ( ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) Fn ( ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) -> ( ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) <-> E. i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) E. r e. ( I X. 2o ) ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) ) )
83 80 81 82 3syl 
 |-  ( ph -> ( ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) <-> E. i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) E. r e. ( I X. 2o ) ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) ) )
84 74 83 mpbid 
 |-  ( ph -> E. i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) E. r e. ( I X. 2o ) ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) )
85 20 simprd 
 |-  ( ph -> ( ( # ` B ) - 1 ) e. NN )
86 1 2 3 4 5 6 efgsdmi 
 |-  ( ( B e. dom S /\ ( ( # ` B ) - 1 ) e. NN ) -> ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
87 9 85 86 syl2anc 
 |-  ( ph -> ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
88 1 2 3 4 5 6 efgsdm 
 |-  ( B e. dom S <-> ( B e. ( Word W \ { (/) } ) /\ ( B ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` B ) ) ( B ` i ) e. ran ( T ` ( B ` ( i - 1 ) ) ) ) )
89 88 simp1bi 
 |-  ( B e. dom S -> B e. ( Word W \ { (/) } ) )
90 9 89 syl 
 |-  ( ph -> B e. ( Word W \ { (/) } ) )
91 90 eldifad 
 |-  ( ph -> B e. Word W )
92 wrdf 
 |-  ( B e. Word W -> B : ( 0 ..^ ( # ` B ) ) --> W )
93 91 92 syl 
 |-  ( ph -> B : ( 0 ..^ ( # ` B ) ) --> W )
94 fzo0end 
 |-  ( ( ( # ` B ) - 1 ) e. NN -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
95 elfzofz 
 |-  ( ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ... ( ( # ` B ) - 1 ) ) )
96 85 94 95 3syl 
 |-  ( ph -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ... ( ( # ` B ) - 1 ) ) )
97 lencl 
 |-  ( B e. Word W -> ( # ` B ) e. NN0 )
98 91 97 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
99 98 nn0zd 
 |-  ( ph -> ( # ` B ) e. ZZ )
100 fzoval 
 |-  ( ( # ` B ) e. ZZ -> ( 0 ..^ ( # ` B ) ) = ( 0 ... ( ( # ` B ) - 1 ) ) )
101 99 100 syl 
 |-  ( ph -> ( 0 ..^ ( # ` B ) ) = ( 0 ... ( ( # ` B ) - 1 ) ) )
102 96 101 eleqtrrd 
 |-  ( ph -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( # ` B ) ) )
103 93 102 ffvelcdmd 
 |-  ( ph -> ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) e. W )
104 1 2 3 4 efgtf 
 |-  ( ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) e. W -> ( ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) = ( a e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) , b e. ( I X. 2o ) |-> ( ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) : ( ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) --> W ) )
105 103 104 syl 
 |-  ( ph -> ( ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) = ( a e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) , b e. ( I X. 2o ) |-> ( ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) : ( ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) --> W ) )
106 105 simprd 
 |-  ( ph -> ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) : ( ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) --> W )
107 ffn 
 |-  ( ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) : ( ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) --> W -> ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) Fn ( ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) )
108 ovelrn 
 |-  ( ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) Fn ( ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) X. ( I X. 2o ) ) -> ( ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) <-> E. j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) E. s e. ( I X. 2o ) ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) )
109 106 107 108 3syl 
 |-  ( ph -> ( ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) <-> E. j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) E. s e. ( I X. 2o ) ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) )
110 87 109 mpbid 
 |-  ( ph -> E. j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) E. s e. ( I X. 2o ) ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) )
111 reeanv 
 |-  ( E. i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) E. j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ( E. r e. ( I X. 2o ) ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ E. s e. ( I X. 2o ) ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) <-> ( E. i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) E. r e. ( I X. 2o ) ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ E. j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) E. s e. ( I X. 2o ) ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) )
112 reeanv 
 |-  ( E. r e. ( I X. 2o ) E. s e. ( I X. 2o ) ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) <-> ( E. r e. ( I X. 2o ) ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ E. s e. ( I X. 2o ) ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) )
113 7 ad3antrrr 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
114 8 ad3antrrr 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> A e. dom S )
115 9 ad3antrrr 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> B e. dom S )
116 10 ad3antrrr 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> ( S ` A ) = ( S ` B ) )
117 11 ad3antrrr 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> -. ( A ` 0 ) = ( B ` 0 ) )
118 eqid 
 |-  ( ( ( # ` A ) - 1 ) - 1 ) = ( ( ( # ` A ) - 1 ) - 1 )
119 eqid 
 |-  ( ( ( # ` B ) - 1 ) - 1 ) = ( ( ( # ` B ) - 1 ) - 1 )
120 simpllr 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) )
121 120 simpld 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) )
122 120 simprd 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) )
123 simplrl 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) )
124 123 simpld 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> r e. ( I X. 2o ) )
125 123 simprd 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> s e. ( I X. 2o ) )
126 simplrr 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) )
127 126 simpld 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) )
128 126 simprd 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) )
129 simpr 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) -> -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
130 1 2 3 4 5 6 113 114 115 116 117 118 119 121 122 124 125 127 128 129 efgredlemb 
 |-  -. ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
131 iman 
 |-  ( ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) <-> -. ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) /\ -. ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
132 130 131 mpbir 
 |-  ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) /\ ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) ) ) -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
133 132 expr 
 |-  ( ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) /\ ( r e. ( I X. 2o ) /\ s e. ( I X. 2o ) ) ) -> ( ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
134 133 rexlimdvva 
 |-  ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) -> ( E. r e. ( I X. 2o ) E. s e. ( I X. 2o ) ( ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
135 112 134 biimtrrid 
 |-  ( ( ph /\ ( i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) /\ j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ) ) -> ( ( E. r e. ( I X. 2o ) ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ E. s e. ( I X. 2o ) ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
136 135 rexlimdvva 
 |-  ( ph -> ( E. i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) E. j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) ( E. r e. ( I X. 2o ) ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ E. s e. ( I X. 2o ) ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
137 111 136 biimtrrid 
 |-  ( ph -> ( ( E. i e. ( 0 ... ( # ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) ) E. r e. ( I X. 2o ) ( S ` A ) = ( i ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) r ) /\ E. j e. ( 0 ... ( # ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) ) E. s e. ( I X. 2o ) ( S ` B ) = ( j ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) s ) ) -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
138 84 110 137 mp2and 
 |-  ( ph -> ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
139 fvres 
 |-  ( ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( ( # ` B ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
140 85 94 139 3syl 
 |-  ( ph -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( ( # ` B ) - 1 ) - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
141 138 70 140 3eqtr4d 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( ( # ` A ) - 1 ) - 1 ) ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
142 fz1ssfz0 
 |-  ( 1 ... ( # ` B ) ) C_ ( 0 ... ( # ` B ) )
143 98 nn0red 
 |-  ( ph -> ( # ` B ) e. RR )
144 143 lem1d 
 |-  ( ph -> ( ( # ` B ) - 1 ) <_ ( # ` B ) )
145 fznn 
 |-  ( ( # ` B ) e. ZZ -> ( ( ( # ` B ) - 1 ) e. ( 1 ... ( # ` B ) ) <-> ( ( ( # ` B ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) <_ ( # ` B ) ) ) )
146 99 145 syl 
 |-  ( ph -> ( ( ( # ` B ) - 1 ) e. ( 1 ... ( # ` B ) ) <-> ( ( ( # ` B ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) <_ ( # ` B ) ) ) )
147 85 144 146 mpbir2and 
 |-  ( ph -> ( ( # ` B ) - 1 ) e. ( 1 ... ( # ` B ) ) )
148 142 147 sselid 
 |-  ( ph -> ( ( # ` B ) - 1 ) e. ( 0 ... ( # ` B ) ) )
149 pfxres 
 |-  ( ( B e. Word W /\ ( ( # ` B ) - 1 ) e. ( 0 ... ( # ` B ) ) ) -> ( B prefix ( ( # ` B ) - 1 ) ) = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) )
150 91 148 149 syl2anc 
 |-  ( ph -> ( B prefix ( ( # ` B ) - 1 ) ) = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) )
151 150 fveq2d 
 |-  ( ph -> ( # ` ( B prefix ( ( # ` B ) - 1 ) ) ) = ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) )
152 pfxlen 
 |-  ( ( B e. Word W /\ ( ( # ` B ) - 1 ) e. ( 0 ... ( # ` B ) ) ) -> ( # ` ( B prefix ( ( # ` B ) - 1 ) ) ) = ( ( # ` B ) - 1 ) )
153 91 148 152 syl2anc 
 |-  ( ph -> ( # ` ( B prefix ( ( # ` B ) - 1 ) ) ) = ( ( # ` B ) - 1 ) )
154 151 153 eqtr3d 
 |-  ( ph -> ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( ( # ` B ) - 1 ) )
155 154 fvoveq1d 
 |-  ( ph -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) - 1 ) ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
156 141 67 155 3eqtr4d 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) - 1 ) ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) - 1 ) ) )
157 1 2 3 4 5 6 efgsres 
 |-  ( ( B e. dom S /\ ( ( # ` B ) - 1 ) e. ( 1 ... ( # ` B ) ) ) -> ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) e. dom S )
158 9 147 157 syl2anc 
 |-  ( ph -> ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) e. dom S )
159 1 2 3 4 5 6 efgsval 
 |-  ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) e. dom S -> ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) - 1 ) ) )
160 158 159 syl 
 |-  ( ph -> ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) - 1 ) ) )
161 156 58 160 3eqtr4d 
 |-  ( ph -> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) )
162 fveq2 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( S ` a ) = ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) )
163 162 fveq2d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( # ` ( S ` a ) ) = ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) )
164 163 breq1d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) <-> ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) ) )
165 162 eqeq1d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( S ` a ) = ( S ` b ) <-> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) ) )
166 fveq1 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( a ` 0 ) = ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) )
167 166 eqeq1d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( a ` 0 ) = ( b ` 0 ) <-> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) )
168 165 167 imbi12d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) <-> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) ) )
169 164 168 imbi12d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) ) ) )
170 fveq2 
 |-  ( b = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( S ` b ) = ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) )
171 170 eqeq2d 
 |-  ( b = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) <-> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) )
172 fveq1 
 |-  ( b = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( b ` 0 ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) )
173 172 eqeq2d 
 |-  ( b = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) <-> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) ) )
174 171 173 imbi12d 
 |-  ( b = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) <-> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) ) ) )
175 174 imbi2d 
 |-  ( b = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) ) ) ) )
176 169 175 rspc2va 
 |-  ( ( ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) e. dom S /\ ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) e. dom S ) /\ A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) -> ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) ) ) )
177 56 158 7 176 syl21anc 
 |-  ( ph -> ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) ) ) )
178 77 161 177 mp2d 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) )
179 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( ( # ` A ) - 1 ) ) <-> ( ( # ` A ) - 1 ) e. NN )
180 21 179 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
181 180 fvresd 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( A ` 0 ) )
182 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( ( # ` B ) - 1 ) ) <-> ( ( # ` B ) - 1 ) e. NN )
183 85 182 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
184 183 fvresd 
 |-  ( ph -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( B ` 0 ) )
185 178 181 184 3eqtr3d 
 |-  ( ph -> ( A ` 0 ) = ( B ` 0 ) )
186 185 11 pm2.65i 
 |-  -. ph