Metamath Proof Explorer


Theorem efgsres

Description: An initial segment of an extension sequence is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-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 ) ) )
Assertion efgsres
|- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) 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 adantr
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> F e. ( Word W \ { (/) } ) )
10 9 eldifad
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> F e. Word W )
11 fz1ssfz0
 |-  ( 1 ... ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
12 simpr
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> N e. ( 1 ... ( # ` F ) ) )
13 11 12 sselid
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> N e. ( 0 ... ( # ` F ) ) )
14 pfxres
 |-  ( ( F e. Word W /\ N e. ( 0 ... ( # ` F ) ) ) -> ( F prefix N ) = ( F |` ( 0 ..^ N ) ) )
15 10 13 14 syl2anc
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F prefix N ) = ( F |` ( 0 ..^ N ) ) )
16 pfxcl
 |-  ( F e. Word W -> ( F prefix N ) e. Word W )
17 10 16 syl
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F prefix N ) e. Word W )
18 15 17 eqeltrrd
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) e. Word W )
19 pfxlen
 |-  ( ( F e. Word W /\ N e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) = N )
20 10 13 19 syl2anc
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) = N )
21 elfznn
 |-  ( N e. ( 1 ... ( # ` F ) ) -> N e. NN )
22 21 adantl
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> N e. NN )
23 20 22 eqeltrd
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) e. NN )
24 wrdfin
 |-  ( ( F prefix N ) e. Word W -> ( F prefix N ) e. Fin )
25 hashnncl
 |-  ( ( F prefix N ) e. Fin -> ( ( # ` ( F prefix N ) ) e. NN <-> ( F prefix N ) =/= (/) ) )
26 17 24 25 3syl
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( ( # ` ( F prefix N ) ) e. NN <-> ( F prefix N ) =/= (/) ) )
27 23 26 mpbid
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F prefix N ) =/= (/) )
28 15 27 eqnetrrd
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) =/= (/) )
29 eldifsn
 |-  ( ( F |` ( 0 ..^ N ) ) e. ( Word W \ { (/) } ) <-> ( ( F |` ( 0 ..^ N ) ) e. Word W /\ ( F |` ( 0 ..^ N ) ) =/= (/) ) )
30 18 28 29 sylanbrc
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) e. ( Word W \ { (/) } ) )
31 lbfzo0
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
32 22 31 sylibr
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> 0 e. ( 0 ..^ N ) )
33 32 fvresd
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( ( F |` ( 0 ..^ N ) ) ` 0 ) = ( F ` 0 ) )
34 7 simp2bi
 |-  ( F e. dom S -> ( F ` 0 ) e. D )
35 34 adantr
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F ` 0 ) e. D )
36 33 35 eqeltrd
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( ( F |` ( 0 ..^ N ) ) ` 0 ) e. D )
37 elfzuz3
 |-  ( N e. ( 1 ... ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
38 37 adantl
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
39 fzoss2
 |-  ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 1 ..^ N ) C_ ( 1 ..^ ( # ` F ) ) )
40 38 39 syl
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( 1 ..^ N ) C_ ( 1 ..^ ( # ` F ) ) )
41 7 simp3bi
 |-  ( F e. dom S -> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
42 41 adantr
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
43 ssralv
 |-  ( ( 1 ..^ N ) C_ ( 1 ..^ ( # ` F ) ) -> ( A. i e. ( 1 ..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) -> A. i e. ( 1 ..^ N ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
44 40 42 43 sylc
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> A. i e. ( 1 ..^ N ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
45 fzo0ss1
 |-  ( 1 ..^ N ) C_ ( 0 ..^ N )
46 45 sseli
 |-  ( i e. ( 1 ..^ N ) -> i e. ( 0 ..^ N ) )
47 46 fvresd
 |-  ( i e. ( 1 ..^ N ) -> ( ( F |` ( 0 ..^ N ) ) ` i ) = ( F ` i ) )
48 elfzoel2
 |-  ( i e. ( 1 ..^ N ) -> N e. ZZ )
49 peano2zm
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
50 48 49 syl
 |-  ( i e. ( 1 ..^ N ) -> ( N - 1 ) e. ZZ )
51 uzid
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
52 48 51 syl
 |-  ( i e. ( 1 ..^ N ) -> N e. ( ZZ>= ` N ) )
53 48 zcnd
 |-  ( i e. ( 1 ..^ N ) -> N e. CC )
54 ax-1cn
 |-  1 e. CC
55 npcan
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
56 53 54 55 sylancl
 |-  ( i e. ( 1 ..^ N ) -> ( ( N - 1 ) + 1 ) = N )
57 56 fveq2d
 |-  ( i e. ( 1 ..^ N ) -> ( ZZ>= ` ( ( N - 1 ) + 1 ) ) = ( ZZ>= ` N ) )
58 52 57 eleqtrrd
 |-  ( i e. ( 1 ..^ N ) -> N e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
59 peano2uzr
 |-  ( ( ( N - 1 ) e. ZZ /\ N e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) ) -> N e. ( ZZ>= ` ( N - 1 ) ) )
60 50 58 59 syl2anc
 |-  ( i e. ( 1 ..^ N ) -> N e. ( ZZ>= ` ( N - 1 ) ) )
61 fzoss2
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
62 60 61 syl
 |-  ( i e. ( 1 ..^ N ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
63 elfzo1elm1fzo0
 |-  ( i e. ( 1 ..^ N ) -> ( i - 1 ) e. ( 0 ..^ ( N - 1 ) ) )
64 62 63 sseldd
 |-  ( i e. ( 1 ..^ N ) -> ( i - 1 ) e. ( 0 ..^ N ) )
65 64 fvresd
 |-  ( i e. ( 1 ..^ N ) -> ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) = ( F ` ( i - 1 ) ) )
66 65 fveq2d
 |-  ( i e. ( 1 ..^ N ) -> ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) = ( T ` ( F ` ( i - 1 ) ) ) )
67 66 rneqd
 |-  ( i e. ( 1 ..^ N ) -> ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) = ran ( T ` ( F ` ( i - 1 ) ) ) )
68 47 67 eleq12d
 |-  ( i e. ( 1 ..^ N ) -> ( ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) <-> ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
69 68 ralbiia
 |-  ( A. i e. ( 1 ..^ N ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) <-> A. i e. ( 1 ..^ N ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
70 44 69 sylibr
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> A. i e. ( 1 ..^ N ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) )
71 15 fveq2d
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` ( F prefix N ) ) = ( # ` ( F |` ( 0 ..^ N ) ) ) )
72 71 20 eqtr3d
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( # ` ( F |` ( 0 ..^ N ) ) ) = N )
73 72 oveq2d
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( 1 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) = ( 1 ..^ N ) )
74 73 raleqdv
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( A. i e. ( 1 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) <-> A. i e. ( 1 ..^ N ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) ) )
75 70 74 mpbird
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> A. i e. ( 1 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) )
76 1 2 3 4 5 6 efgsdm
 |-  ( ( F |` ( 0 ..^ N ) ) e. dom S <-> ( ( F |` ( 0 ..^ N ) ) e. ( Word W \ { (/) } ) /\ ( ( F |` ( 0 ..^ N ) ) ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) ( ( F |` ( 0 ..^ N ) ) ` i ) e. ran ( T ` ( ( F |` ( 0 ..^ N ) ) ` ( i - 1 ) ) ) ) )
77 30 36 75 76 syl3anbrc
 |-  ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) e. dom S )