Metamath Proof Explorer

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 ⊢ φ → S ∈ V
sseqval.2 ⊢ φ → M ∈ Word S
sseqval.3 ⊢ W = Word S ∩ . -1 ℤ ≥ M
sseqval.4 ⊢ φ → F : W ⟶ S
Assertion sseqfres ⊢ φ → M seq str F ↾ 0 ..^ M = M

Proof

Step Hyp Ref Expression
1 sseqval.1 ⊢ φ → S ∈ V
2 sseqval.2 ⊢ φ → M ∈ Word S
3 sseqval.3 ⊢ W = Word S ∩ . -1 ℤ ≥ M
4 sseqval.4 ⊢ φ → F : W ⟶ S
5 1 adantr ⊢ φ ∧ i ∈ 0 ..^ M → S ∈ V
6 2 adantr ⊢ φ ∧ i ∈ 0 ..^ M → M ∈ Word S
7 4 adantr ⊢ φ ∧ i ∈ 0 ..^ M → F : W ⟶ S
8 simpr ⊢ φ ∧ i ∈ 0 ..^ M → i ∈ 0 ..^ M
9 5 6 3 7 8 sseqfv1 ⊢ φ ∧ i ∈ 0 ..^ M → M seq str F ⁡ i = M ⁡ i
10 9 ralrimiva ⊢ φ → ∀ i ∈ 0 ..^ M M seq str F ⁡ i = M ⁡ i
11 1 2 3 4 sseqfn ⊢ φ → M seq str F Fn ℕ 0
12 wrdfn ⊢ M ∈ Word S → M Fn 0 ..^ M
13 2 12 syl ⊢ φ → M Fn 0 ..^ M
14 fzo0ssnn0 ⊢ 0 ..^ M ⊆ ℕ 0
15 14 a1i ⊢ φ → 0 ..^ M ⊆ ℕ 0
16 fvreseq1 ⊢ M seq str F Fn ℕ 0 ∧ M Fn 0 ..^ M ∧ 0 ..^ M ⊆ ℕ 0 → M seq str F ↾ 0 ..^ M = M ↔ ∀ i ∈ 0 ..^ M M seq str F ⁡ i = M ⁡ i
17 11 13 15 16 syl21anc ⊢ φ → M seq str F ↾ 0 ..^ M = M ↔ ∀ i ∈ 0 ..^ M M seq str F ⁡ i = M ⁡ i
18 10 17 mpbird ⊢ φ → M seq str F ↾ 0 ..^ M = M