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	⊢ ( 𝜑 → 𝑆 ∈ V )
	sseqval.2	⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
	sseqval.3	⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
	sseqval.4	⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
Assertion	sseqfres	⊢ ( 𝜑 → ( ( 𝑀 seqstr 𝐹 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	⊢ ( 𝜑 → 𝑆 ∈ V )
2		sseqval.2	⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
3		sseqval.3	⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
4		sseqval.4	⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) → 𝑆 ∈ V )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) → 𝑀 ∈ Word 𝑆 )
7	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) → 𝐹 : 𝑊 ⟶ 𝑆 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) )
9	5 6 3 7 8	sseqfv1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) → ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑖 ) = ( 𝑀 ‘ 𝑖 ) )
10	9	ralrimiva	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑖 ) = ( 𝑀 ‘ 𝑖 ) )
11	1 2 3 4	sseqfn	⊢ ( 𝜑 → ( 𝑀 seqstr 𝐹 ) Fn ℕ0 )
12		wrdfn	⊢ ( 𝑀 ∈ Word 𝑆 → 𝑀 Fn ( 0 ..^ ( ♯ ‘ 𝑀 ) ) )
13	2 12	syl	⊢ ( 𝜑 → 𝑀 Fn ( 0 ..^ ( ♯ ‘ 𝑀 ) ) )
14		fzo0ssnn0	⊢ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ⊆ ℕ0
15	14	a1i	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ⊆ ℕ0 )
16		fvreseq1	⊢ ( ( ( ( 𝑀 seqstr 𝐹 ) Fn ℕ0 ∧ 𝑀 Fn ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) ∧ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ⊆ ℕ0 ) → ( ( ( 𝑀 seqstr 𝐹 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) = 𝑀 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑖 ) = ( 𝑀 ‘ 𝑖 ) ) )
17	11 13 15 16	syl21anc	⊢ ( 𝜑 → ( ( ( 𝑀 seqstr 𝐹 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) = 𝑀 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑖 ) = ( 𝑀 ‘ 𝑖 ) ) )
18	10 17	mpbird	⊢ ( 𝜑 → ( ( 𝑀 seqstr 𝐹 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) = 𝑀 )