Metamath Proof Explorer

Theorem efgsp1

Description: If F is an extension sequence and A is an extension of the last element of F , then F + <" A "> is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015)

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 ) ) )
Assertion efgsp1 
|- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F ++ <" A "> ) e. dom S )

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 1 2 3 4 5 6 efgsdm 
 |-  ( F e. dom S <-> ( F e. ( Word W \ { (/) } ) /\ ( F ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
8 7 simp1bi 
 |-  ( F e. dom S -> F e. ( Word W \ { (/) } ) )
9 8 eldifad 
 |-  ( F e. dom S -> F e. Word W )
10 1 2 3 4 5 6 efgsf 
 |-  S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W
11 10 fdmi 
 |-  dom S = { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) }
12 11 feq2i 
 |-  ( S : dom S --> W <-> S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W )
13 10 12 mpbir 
 |-  S : dom S --> W
14 13 ffvelrni 
 |-  ( F e. dom S -> ( S ` F ) e. W )
15 1 2 3 4 efgtf 
 |-  ( ( S ` F ) e. W -> ( ( T ` ( S ` F ) ) = ( a e. ( 0 ... ( # ` ( S ` F ) ) ) , i e. ( I X. 2o ) |-> ( ( S ` F ) splice <. a , a , <" i ( M ` i ) "> >. ) ) /\ ( T ` ( S ` F ) ) : ( ( 0 ... ( # ` ( S ` F ) ) ) X. ( I X. 2o ) ) --> W ) )
16 14 15 syl 
 |-  ( F e. dom S -> ( ( T ` ( S ` F ) ) = ( a e. ( 0 ... ( # ` ( S ` F ) ) ) , i e. ( I X. 2o ) |-> ( ( S ` F ) splice <. a , a , <" i ( M ` i ) "> >. ) ) /\ ( T ` ( S ` F ) ) : ( ( 0 ... ( # ` ( S ` F ) ) ) X. ( I X. 2o ) ) --> W ) )
17 16 simprd 
 |-  ( F e. dom S -> ( T ` ( S ` F ) ) : ( ( 0 ... ( # ` ( S ` F ) ) ) X. ( I X. 2o ) ) --> W )
18 17 frnd 
 |-  ( F e. dom S -> ran ( T ` ( S ` F ) ) C_ W )
19 18 sselda 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A e. W )
20 19 s1cld 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> <" A "> e. Word W )
21 ccatcl 
 |-  ( ( F e. Word W /\ <" A "> e. Word W ) -> ( F ++ <" A "> ) e. Word W )
22 9 20 21 syl2an2r 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F ++ <" A "> ) e. Word W )
23 ccatws1n0 
 |-  ( F e. Word W -> ( F ++ <" A "> ) =/= (/) )
24 9 23 syl 
 |-  ( F e. dom S -> ( F ++ <" A "> ) =/= (/) )
25 24 adantr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F ++ <" A "> ) =/= (/) )
26 eldifsn 
 |-  ( ( F ++ <" A "> ) e. ( Word W \ { (/) } ) <-> ( ( F ++ <" A "> ) e. Word W /\ ( F ++ <" A "> ) =/= (/) ) )
27 22 25 26 sylanbrc 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F ++ <" A "> ) e. ( Word W \ { (/) } ) )
28 9 adantr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> F e. Word W )
29 eldifsni 
 |-  ( F e. ( Word W \ { (/) } ) -> F =/= (/) )
30 8 29 syl 
 |-  ( F e. dom S -> F =/= (/) )
31 len0nnbi 
 |-  ( F e. Word W -> ( F =/= (/) <-> ( # ` F ) e. NN ) )
32 9 31 syl 
 |-  ( F e. dom S -> ( F =/= (/) <-> ( # ` F ) e. NN ) )
33 30 32 mpbid 
 |-  ( F e. dom S -> ( # ` F ) e. NN )
34 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` F ) ) <-> ( # ` F ) e. NN )
35 33 34 sylibr 
 |-  ( F e. dom S -> 0 e. ( 0 ..^ ( # ` F ) ) )
36 35 adantr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
37 ccatval1 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ 0 e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F ++ <" A "> ) ` 0 ) = ( F ` 0 ) )
38 28 20 36 37 syl3anc 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F ++ <" A "> ) ` 0 ) = ( F ` 0 ) )
39 7 simp2bi 
 |-  ( F e. dom S -> ( F ` 0 ) e. D )
40 39 adantr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F ` 0 ) e. D )
41 38 40 eqeltrd 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F ++ <" A "> ) ` 0 ) e. D )
42 7 simp3bi 
 |-  ( F e. dom S -> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
43 42 adantr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
44 fzo0ss1 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) )
45 44 sseli 
 |-  ( i e. ( 1 ..^ ( # ` F ) ) -> i e. ( 0 ..^ ( # ` F ) ) )
46 ccatval1 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F ++ <" A "> ) ` i ) = ( F ` i ) )
47 45 46 syl3an3 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1 ..^ ( # ` F ) ) ) -> ( ( F ++ <" A "> ) ` i ) = ( F ` i ) )
48 elfzoel2 
 |-  ( i e. ( 1 ..^ ( # ` F ) ) -> ( # ` F ) e. ZZ )
49 peano2zm 
 |-  ( ( # ` F ) e. ZZ -> ( ( # ` F ) - 1 ) e. ZZ )
50 48 49 syl 
 |-  ( i e. ( 1 ..^ ( # ` F ) ) -> ( ( # ` F ) - 1 ) e. ZZ )
51 48 zred 
 |-  ( i e. ( 1 ..^ ( # ` F ) ) -> ( # ` F ) e. RR )
52 51 lem1d 
 |-  ( i e. ( 1 ..^ ( # ` F ) ) -> ( ( # ` F ) - 1 ) <_ ( # ` F ) )
53 eluz2 
 |-  ( ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) <-> ( ( ( # ` F ) - 1 ) e. ZZ /\ ( # ` F ) e. ZZ /\ ( ( # ` F ) - 1 ) <_ ( # ` F ) ) )
54 50 48 52 53 syl3anbrc 
 |-  ( i e. ( 1 ..^ ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) )
55 fzoss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
56 54 55 syl 
 |-  ( i e. ( 1 ..^ ( # ` F ) ) -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
57 elfzo1elm1fzo0 
 |-  ( i e. ( 1 ..^ ( # ` F ) ) -> ( i - 1 ) e. ( 0 ..^ ( ( # ` F ) - 1 ) ) )
58 56 57 sseldd 
 |-  ( i e. ( 1 ..^ ( # ` F ) ) -> ( i - 1 ) e. ( 0 ..^ ( # ` F ) ) )
59 ccatval1 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ ( i - 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F ++ <" A "> ) ` ( i - 1 ) ) = ( F ` ( i - 1 ) ) )
60 58 59 syl3an3 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1 ..^ ( # ` F ) ) ) -> ( ( F ++ <" A "> ) ` ( i - 1 ) ) = ( F ` ( i - 1 ) ) )
61 60 fveq2d 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1 ..^ ( # ` F ) ) ) -> ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) = ( T ` ( F ` ( i - 1 ) ) ) )
62 61 rneqd 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1 ..^ ( # ` F ) ) ) -> ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) = ran ( T ` ( F ` ( i - 1 ) ) ) )
63 47 62 eleq12d 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) <-> ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
64 63 3expa 
 |-  ( ( ( F e. Word W /\ <" A "> e. Word W ) /\ i e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) <-> ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
65 64 ralbidva 
 |-  ( ( F e. Word W /\ <" A "> e. Word W ) -> ( A. i e. ( 1 ..^ ( # ` F ) ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) <-> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
66 9 20 65 syl2an2r 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( A. i e. ( 1 ..^ ( # ` F ) ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) <-> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
67 43 66 mpbird 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. ( 1 ..^ ( # ` F ) ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) )
68 lencl 
 |-  ( F e. Word W -> ( # ` F ) e. NN0 )
69 9 68 syl 
 |-  ( F e. dom S -> ( # ` F ) e. NN0 )
70 69 nn0cnd 
 |-  ( F e. dom S -> ( # ` F ) e. CC )
71 70 addid2d 
 |-  ( F e. dom S -> ( 0 + ( # ` F ) ) = ( # ` F ) )
72 71 fveq2d 
 |-  ( F e. dom S -> ( ( F ++ <" A "> ) ` ( 0 + ( # ` F ) ) ) = ( ( F ++ <" A "> ) ` ( # ` F ) ) )
73 72 adantr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F ++ <" A "> ) ` ( 0 + ( # ` F ) ) ) = ( ( F ++ <" A "> ) ` ( # ` F ) ) )
74 s1len 
 |-  ( # ` <" A "> ) = 1
75 1nn 
 |-  1 e. NN
76 74 75 eqeltri 
 |-  ( # ` <" A "> ) e. NN
77 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` <" A "> ) ) <-> ( # ` <" A "> ) e. NN )
78 76 77 mpbir 
 |-  0 e. ( 0 ..^ ( # ` <" A "> ) )
79 78 a1i 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> 0 e. ( 0 ..^ ( # ` <" A "> ) ) )
80 ccatval3 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ 0 e. ( 0 ..^ ( # ` <" A "> ) ) ) -> ( ( F ++ <" A "> ) ` ( 0 + ( # ` F ) ) ) = ( <" A "> ` 0 ) )
81 28 20 79 80 syl3anc 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F ++ <" A "> ) ` ( 0 + ( # ` F ) ) ) = ( <" A "> ` 0 ) )
82 73 81 eqtr3d 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F ++ <" A "> ) ` ( # ` F ) ) = ( <" A "> ` 0 ) )
83 simpr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A e. ran ( T ` ( S ` F ) ) )
84 s1fv 
 |-  ( A e. ran ( T ` ( S ` F ) ) -> ( <" A "> ` 0 ) = A )
85 84 adantl 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( <" A "> ` 0 ) = A )
86 fzo0end 
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
87 33 86 syl 
 |-  ( F e. dom S -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
88 87 adantr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
89 ccatval1 
 |-  ( ( F e. Word W /\ <" A "> e. Word W /\ ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) = ( F ` ( ( # ` F ) - 1 ) ) )
90 28 20 88 89 syl3anc 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) = ( F ` ( ( # ` F ) - 1 ) ) )
91 1 2 3 4 5 6 efgsval 
 |-  ( F e. dom S -> ( S ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
92 91 adantr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( S ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
93 90 92 eqtr4d 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) = ( S ` F ) )
94 93 fveq2d 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( T ` ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) ) = ( T ` ( S ` F ) ) )
95 94 rneqd 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ran ( T ` ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) ) = ran ( T ` ( S ` F ) ) )
96 83 85 95 3eltr4d 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( <" A "> ` 0 ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
97 82 96 eqeltrd 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F ++ <" A "> ) ` ( # ` F ) ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
98 fvex 
 |-  ( # ` F ) e. _V
99 fveq2 
 |-  ( i = ( # ` F ) -> ( ( F ++ <" A "> ) ` i ) = ( ( F ++ <" A "> ) ` ( # ` F ) ) )
100 fvoveq1 
 |-  ( i = ( # ` F ) -> ( ( F ++ <" A "> ) ` ( i - 1 ) ) = ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) )
101 100 fveq2d 
 |-  ( i = ( # ` F ) -> ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) = ( T ` ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
102 101 rneqd 
 |-  ( i = ( # ` F ) -> ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) = ran ( T ` ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
103 99 102 eleq12d 
 |-  ( i = ( # ` F ) -> ( ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) <-> ( ( F ++ <" A "> ) ` ( # ` F ) ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) ) ) )
104 98 103 ralsn 
 |-  ( A. i e. { ( # ` F ) } ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) <-> ( ( F ++ <" A "> ) ` ( # ` F ) ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
105 97 104 sylibr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. { ( # ` F ) } ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) )
106 ralunb 
 |-  ( A. i e. ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) <-> ( A. i e. ( 1 ..^ ( # ` F ) ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) /\ A. i e. { ( # ` F ) } ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) ) )
107 67 105 106 sylanbrc 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) )
108 ccatlen 
 |-  ( ( F e. Word W /\ <" A "> e. Word W ) -> ( # ` ( F ++ <" A "> ) ) = ( ( # ` F ) + ( # ` <" A "> ) ) )
109 9 20 108 syl2an2r 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` ( F ++ <" A "> ) ) = ( ( # ` F ) + ( # ` <" A "> ) ) )
110 74 oveq2i 
 |-  ( ( # ` F ) + ( # ` <" A "> ) ) = ( ( # ` F ) + 1 )
111 109 110 eqtrdi 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` ( F ++ <" A "> ) ) = ( ( # ` F ) + 1 ) )
112 111 oveq2d 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 1 ..^ ( # ` ( F ++ <" A "> ) ) ) = ( 1 ..^ ( ( # ` F ) + 1 ) ) )
113 nnuz 
 |-  NN = ( ZZ>= ` 1 )
114 33 113 eleqtrdi 
 |-  ( F e. dom S -> ( # ` F ) e. ( ZZ>= ` 1 ) )
115 fzosplitsn 
 |-  ( ( # ` F ) e. ( ZZ>= ` 1 ) -> ( 1 ..^ ( ( # ` F ) + 1 ) ) = ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) )
116 114 115 syl 
 |-  ( F e. dom S -> ( 1 ..^ ( ( # ` F ) + 1 ) ) = ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) )
117 116 adantr 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 1 ..^ ( ( # ` F ) + 1 ) ) = ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) )
118 112 117 eqtrd 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 1 ..^ ( # ` ( F ++ <" A "> ) ) ) = ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) )
119 118 raleqdv 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( A. i e. ( 1 ..^ ( # ` ( F ++ <" A "> ) ) ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) <-> A. i e. ( ( 1 ..^ ( # ` F ) ) u. { ( # ` F ) } ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) ) )
120 107 119 mpbird 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. ( 1 ..^ ( # ` ( F ++ <" A "> ) ) ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) )
121 1 2 3 4 5 6 efgsdm 
 |-  ( ( F ++ <" A "> ) e. dom S <-> ( ( F ++ <" A "> ) e. ( Word W \ { (/) } ) /\ ( ( F ++ <" A "> ) ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` ( F ++ <" A "> ) ) ) ( ( F ++ <" A "> ) ` i ) e. ran ( T ` ( ( F ++ <" A "> ) ` ( i - 1 ) ) ) ) )
122 27 41 120 121 syl3anbrc 
 |-  ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F ++ <" A "> ) e. dom S )