Theorem sseqfres

Description: The first elements in the strong recursive sequence are the sequence initializer. (Contributed by Thierry Arnoux, 23-Apr-2019)

	Ref	Expression
Hypotheses	sseqval.1	|- ( ph -> S e. _V )
	sseqval.2	|- ( ph -> M e. Word S )
	sseqval.3	|- W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
	sseqval.4	|- ( ph -> F : W --> S )
Assertion	sseqfres	|- ( ph -> ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) = M )

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	|- ( ph -> S e. _V )
2		sseqval.2	|- ( ph -> M e. Word S )
3		sseqval.3	|- W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
4		sseqval.4	|- ( ph -> F : W --> S )
5	1	adantr	|- ( ( ph /\ i e. ( 0 ..^ ( # ` M ) ) ) -> S e. _V )
6	2	adantr	|- ( ( ph /\ i e. ( 0 ..^ ( # ` M ) ) ) -> M e. Word S )
7	4	adantr	|- ( ( ph /\ i e. ( 0 ..^ ( # ` M ) ) ) -> F : W --> S )
8		simpr	|- ( ( ph /\ i e. ( 0 ..^ ( # ` M ) ) ) -> i e. ( 0 ..^ ( # ` M ) ) )
9	5 6 3 7 8	sseqfv1	|- ( ( ph /\ i e. ( 0 ..^ ( # ` M ) ) ) -> ( ( M seqstr F ) ` i ) = ( M ` i ) )
10	9	ralrimiva	|- ( ph -> A. i e. ( 0 ..^ ( # ` M ) ) ( ( M seqstr F ) ` i ) = ( M ` i ) )
11	1 2 3 4	sseqfn	|- ( ph -> ( M seqstr F ) Fn NN0 )
12		wrdfn	|- ( M e. Word S -> M Fn ( 0 ..^ ( # ` M ) ) )
13	2 12	syl	|- ( ph -> M Fn ( 0 ..^ ( # ` M ) ) )
14		fzo0ssnn0	|- ( 0 ..^ ( # ` M ) ) C_ NN0
15	14	a1i	|- ( ph -> ( 0 ..^ ( # ` M ) ) C_ NN0 )
16		fvreseq1	|- ( ( ( ( M seqstr F ) Fn NN0 /\ M Fn ( 0 ..^ ( # ` M ) ) ) /\ ( 0 ..^ ( # ` M ) ) C_ NN0 ) -> ( ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) = M <-> A. i e. ( 0 ..^ ( # ` M ) ) ( ( M seqstr F ) ` i ) = ( M ` i ) ) )
17	11 13 15 16	syl21anc	|- ( ph -> ( ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) = M <-> A. i e. ( 0 ..^ ( # ` M ) ) ( ( M seqstr F ) ` i ) = ( M ` i ) ) )
18	10 17	mpbird	|- ( ph -> ( ( M seqstr F ) |` ( 0 ..^ ( # ` M ) ) ) = M )