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	ffvelcdmi	|- ( 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	addlidd	|- ( 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	107 118	raleqtrrdv	|- ( ( 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 ) ) ) )
120	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 ) ) ) ) )
121	27 41 119 120	syl3anbrc	|- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F ++ <" A "> ) e. dom S )