Metamath Proof Explorer

Theorem sseqp1

Description: Value of the strong sequence builder function at a successor. (Contributed by Thierry Arnoux, 24-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
sseqfv2.4 ⊢ φ → N ∈ ℤ ≥ M
Assertion sseqp1 ⊢ φ → M seq str F ⁡ N = F ⁡ M seq str F ↾ 0 ..^ N

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 sseqfv2.4 ⊢ φ → N ∈ ℤ ≥ M
6 1 2 3 4 5 sseqfv2 ⊢ φ → M seq str F ⁡ N = lastS ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N
7 fveq2 ⊢ i = M → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M
8 oveq2 ⊢ i = M → 0 ..^ i = 0 ..^ M
9 8 reseq2d ⊢ i = M → M seq str F ↾ 0 ..^ i = M seq str F ↾ 0 ..^ M
10 9 fveq2d ⊢ i = M → F ⁡ M seq str F ↾ 0 ..^ i = F ⁡ M seq str F ↾ 0 ..^ M
11 10 s1eqd ⊢ i = M → ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ = ⟨“ F ⁡ M seq str F ↾ 0 ..^ M ”⟩
12 9 11 oveq12d ⊢ i = M → M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ = M seq str F ↾ 0 ..^ M ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ M ”⟩
13 7 12 eqeq12d ⊢ i = M → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ ↔ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M = M seq str F ↾ 0 ..^ M ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ M ”⟩
14 13 imbi2d ⊢ i = M → φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ ↔ φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M = M seq str F ↾ 0 ..^ M ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ M ”⟩
15 fveq2 ⊢ i = n → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n
16 oveq2 ⊢ i = n → 0 ..^ i = 0 ..^ n
17 16 reseq2d ⊢ i = n → M seq str F ↾ 0 ..^ i = M seq str F ↾ 0 ..^ n
18 17 fveq2d ⊢ i = n → F ⁡ M seq str F ↾ 0 ..^ i = F ⁡ M seq str F ↾ 0 ..^ n
19 18 s1eqd ⊢ i = n → ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ = ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩
20 17 19 oveq12d ⊢ i = n → M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩
21 15 20 eqeq12d ⊢ i = n → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ ↔ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩
22 21 imbi2d ⊢ i = n → φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ ↔ φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩
23 fveq2 ⊢ i = n + 1 → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1
24 oveq2 ⊢ i = n + 1 → 0 ..^ i = 0 ..^ n + 1
25 24 reseq2d ⊢ i = n + 1 → M seq str F ↾ 0 ..^ i = M seq str F ↾ 0 ..^ n + 1
26 25 fveq2d ⊢ i = n + 1 → F ⁡ M seq str F ↾ 0 ..^ i = F ⁡ M seq str F ↾ 0 ..^ n + 1
27 26 s1eqd ⊢ i = n + 1 → ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ = ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
28 25 27 oveq12d ⊢ i = n + 1 → M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ = M seq str F ↾ 0 ..^ n + 1 ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
29 23 28 eqeq12d ⊢ i = n + 1 → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ ↔ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = M seq str F ↾ 0 ..^ n + 1 ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
30 29 imbi2d ⊢ i = n + 1 → φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ ↔ φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = M seq str F ↾ 0 ..^ n + 1 ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
31 fveq2 ⊢ i = N → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N
32 oveq2 ⊢ i = N → 0 ..^ i = 0 ..^ N
33 32 reseq2d ⊢ i = N → M seq str F ↾ 0 ..^ i = M seq str F ↾ 0 ..^ N
34 33 fveq2d ⊢ i = N → F ⁡ M seq str F ↾ 0 ..^ i = F ⁡ M seq str F ↾ 0 ..^ N
35 34 s1eqd ⊢ i = N → ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ = ⟨“ F ⁡ M seq str F ↾ 0 ..^ N ”⟩
36 33 35 oveq12d ⊢ i = N → M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ = M seq str F ↾ 0 ..^ N ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ N ”⟩
37 31 36 eqeq12d ⊢ i = N → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ ↔ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N = M seq str F ↾ 0 ..^ N ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ N ”⟩
38 37 imbi2d ⊢ i = N → φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ i = M seq str F ↾ 0 ..^ i ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ i ”⟩ ↔ φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N = M seq str F ↾ 0 ..^ N ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ N ”⟩
39 ovex ⊢ M ++ ⟨“ F ⁡ M ”⟩ ∈ V
40 lencl ⊢ M ∈ Word S → M ∈ ℕ 0
41 2 40 syl ⊢ φ → M ∈ ℕ 0
42 fvconst2g ⊢ M ++ ⟨“ F ⁡ M ”⟩ ∈ V ∧ M ∈ ℕ 0 → ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M = M ++ ⟨“ F ⁡ M ”⟩
43 39 41 42 sylancr ⊢ φ → ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M = M ++ ⟨“ F ⁡ M ”⟩
44 40 nn0zd ⊢ M ∈ Word S → M ∈ ℤ
45 seq1 ⊢ M ∈ ℤ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M = ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M
46 2 44 45 3syl ⊢ φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M = ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M
47 1 2 3 4 sseqfres ⊢ φ → M seq str F ↾ 0 ..^ M = M
48 47 fveq2d ⊢ φ → F ⁡ M seq str F ↾ 0 ..^ M = F ⁡ M
49 48 s1eqd ⊢ φ → ⟨“ F ⁡ M seq str F ↾ 0 ..^ M ”⟩ = ⟨“ F ⁡ M ”⟩
50 47 49 oveq12d ⊢ φ → M seq str F ↾ 0 ..^ M ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ M ”⟩ = M ++ ⟨“ F ⁡ M ”⟩
51 43 46 50 3eqtr4d ⊢ φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M = M seq str F ↾ 0 ..^ M ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ M ”⟩
52 51 a1i ⊢ M ∈ ℤ → φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M = M seq str F ↾ 0 ..^ M ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ M ”⟩
53 seqp1 ⊢ n ∈ ℤ ≥ M → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1
54 53 adantl ⊢ φ ∧ n ∈ ℤ ≥ M → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1
55 id ⊢ x = a → x = a
56 fveq2 ⊢ x = a → F ⁡ x = F ⁡ a
57 56 s1eqd ⊢ x = a → ⟨“ F ⁡ x ”⟩ = ⟨“ F ⁡ a ”⟩
58 55 57 oveq12d ⊢ x = a → x ++ ⟨“ F ⁡ x ”⟩ = a ++ ⟨“ F ⁡ a ”⟩
59 eqidd ⊢ y = b → a ++ ⟨“ F ⁡ a ”⟩ = a ++ ⟨“ F ⁡ a ”⟩
60 58 59 cbvmpov ⊢ x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ = a ∈ V , b ∈ V ⟼ a ++ ⟨“ F ⁡ a ”⟩
61 60 a1i ⊢ φ ∧ n ∈ ℤ ≥ M → x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ = a ∈ V , b ∈ V ⟼ a ++ ⟨“ F ⁡ a ”⟩
62 simprl ⊢ φ ∧ n ∈ ℤ ≥ M ∧ a = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ∧ b = ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 → a = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n
63 62 fveq2d ⊢ φ ∧ n ∈ ℤ ≥ M ∧ a = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ∧ b = ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 → F ⁡ a = F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n
64 63 s1eqd ⊢ φ ∧ n ∈ ℤ ≥ M ∧ a = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ∧ b = ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 → ⟨“ F ⁡ a ”⟩ = ⟨“ F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ”⟩
65 62 64 oveq12d ⊢ φ ∧ n ∈ ℤ ≥ M ∧ a = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ∧ b = ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 → a ++ ⟨“ F ⁡ a ”⟩ = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ++ ⟨“ F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ”⟩
66 fvexd ⊢ φ ∧ n ∈ ℤ ≥ M → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ∈ V
67 fvexd ⊢ φ ∧ n ∈ ℤ ≥ M → ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 ∈ V
68 ovex ⊢ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ++ ⟨“ F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ”⟩ ∈ V
69 68 a1i ⊢ φ ∧ n ∈ ℤ ≥ M → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ++ ⟨“ F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ”⟩ ∈ V
70 61 65 66 67 69 ovmpod ⊢ φ ∧ n ∈ ℤ ≥ M → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ++ ⟨“ F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ”⟩
71 54 70 eqtrd ⊢ φ ∧ n ∈ ℤ ≥ M → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ++ ⟨“ F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ”⟩
72 71 adantr ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ++ ⟨“ F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ”⟩
73 1 adantr ⊢ φ ∧ n ∈ ℤ ≥ M → S ∈ V
74 2 adantr ⊢ φ ∧ n ∈ ℤ ≥ M → M ∈ Word S
75 4 adantr ⊢ φ ∧ n ∈ ℤ ≥ M → F : W ⟶ S
76 simpr ⊢ φ ∧ n ∈ ℤ ≥ M → n ∈ ℤ ≥ M
77 73 74 3 75 76 sseqfv2 ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F ⁡ n = lastS ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n
78 77 adantr ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → M seq str F ⁡ n = lastS ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n
79 simpr ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩
80 79 fveq2d ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → lastS ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = lastS ⁡ M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩
81 1 2 3 4 sseqf ⊢ φ → M seq str F : ℕ 0 ⟶ S
82 fzo0ssnn0 ⊢ 0 ..^ n ⊆ ℕ 0
83 fssres ⊢ M seq str F : ℕ 0 ⟶ S ∧ 0 ..^ n ⊆ ℕ 0 → M seq str F ↾ 0 ..^ n : 0 ..^ n ⟶ S
84 81 82 83 sylancl ⊢ φ → M seq str F ↾ 0 ..^ n : 0 ..^ n ⟶ S
85 iswrdi ⊢ M seq str F ↾ 0 ..^ n : 0 ..^ n ⟶ S → M seq str F ↾ 0 ..^ n ∈ Word S
86 84 85 syl ⊢ φ → M seq str F ↾ 0 ..^ n ∈ Word S
87 86 adantr ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F ↾ 0 ..^ n ∈ Word S
88 elex ⊢ M seq str F ↾ 0 ..^ n ∈ Word S → M seq str F ↾ 0 ..^ n ∈ V
89 87 88 syl ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F ↾ 0 ..^ n ∈ V
90 81 adantr ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F : ℕ 0 ⟶ S
91 eluznn0 ⊢ M ∈ ℕ 0 ∧ n ∈ ℤ ≥ M → n ∈ ℕ 0
92 41 91 sylan ⊢ φ ∧ n ∈ ℤ ≥ M → n ∈ ℕ 0
93 73 90 92 subiwrdlen ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F ↾ 0 ..^ n = n
94 93 76 eqeltrd ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F ↾ 0 ..^ n ∈ ℤ ≥ M
95 hashf ⊢ . : V ⟶ ℕ 0 ∪ +∞
96 ffn ⊢ . : V ⟶ ℕ 0 ∪ +∞ → . Fn V
97 elpreima ⊢ . Fn V → M seq str F ↾ 0 ..^ n ∈ . -1 ℤ ≥ M ↔ M seq str F ↾ 0 ..^ n ∈ V ∧ M seq str F ↾ 0 ..^ n ∈ ℤ ≥ M
98 95 96 97 mp2b ⊢ M seq str F ↾ 0 ..^ n ∈ . -1 ℤ ≥ M ↔ M seq str F ↾ 0 ..^ n ∈ V ∧ M seq str F ↾ 0 ..^ n ∈ ℤ ≥ M
99 89 94 98 sylanbrc ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F ↾ 0 ..^ n ∈ . -1 ℤ ≥ M
100 87 99 elind ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F ↾ 0 ..^ n ∈ Word S ∩ . -1 ℤ ≥ M
101 100 3 eleqtrrdi ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F ↾ 0 ..^ n ∈ W
102 75 101 ffvelcdmd ⊢ φ ∧ n ∈ ℤ ≥ M → F ⁡ M seq str F ↾ 0 ..^ n ∈ S
103 lswccats1 ⊢ M seq str F ↾ 0 ..^ n ∈ Word S ∧ F ⁡ M seq str F ↾ 0 ..^ n ∈ S → lastS ⁡ M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ = F ⁡ M seq str F ↾ 0 ..^ n
104 87 102 103 syl2anc ⊢ φ ∧ n ∈ ℤ ≥ M → lastS ⁡ M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ = F ⁡ M seq str F ↾ 0 ..^ n
105 104 adantr ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → lastS ⁡ M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ = F ⁡ M seq str F ↾ 0 ..^ n
106 78 80 105 3eqtrrd ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → F ⁡ M seq str F ↾ 0 ..^ n = M seq str F ⁡ n
107 106 s1eqd ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ = ⟨“ M seq str F ⁡ n ”⟩
108 107 oveq2d ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ = M seq str F ↾ 0 ..^ n ++ ⟨“ M seq str F ⁡ n ”⟩
109 73 90 92 iwrdsplit ⊢ φ ∧ n ∈ ℤ ≥ M → M seq str F ↾ 0 ..^ n + 1 = M seq str F ↾ 0 ..^ n ++ ⟨“ M seq str F ⁡ n ”⟩
110 109 adantr ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → M seq str F ↾ 0 ..^ n + 1 = M seq str F ↾ 0 ..^ n ++ ⟨“ M seq str F ⁡ n ”⟩
111 108 79 110 3eqtr4d ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n + 1
112 111 fveq2d ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = F ⁡ M seq str F ↾ 0 ..^ n + 1
113 112 s1eqd ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → ⟨“ F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ”⟩ = ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
114 111 113 oveq12d ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ++ ⟨“ F ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n ”⟩ = M seq str F ↾ 0 ..^ n + 1 ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
115 72 114 eqtrd ⊢ φ ∧ n ∈ ℤ ≥ M ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = M seq str F ↾ 0 ..^ n + 1 ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
116 115 ex ⊢ φ ∧ n ∈ ℤ ≥ M → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = M seq str F ↾ 0 ..^ n + 1 ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
117 116 expcom ⊢ n ∈ ℤ ≥ M → φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = M seq str F ↾ 0 ..^ n + 1 ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
118 117 a2d ⊢ n ∈ ℤ ≥ M → φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n = M seq str F ↾ 0 ..^ n ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n ”⟩ → φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ n + 1 = M seq str F ↾ 0 ..^ n + 1 ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ n + 1 ”⟩
119 14 22 30 38 52 118 uzind4 ⊢ N ∈ ℤ ≥ M → φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N = M seq str F ↾ 0 ..^ N ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ N ”⟩
120 5 119 mpcom ⊢ φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N = M seq str F ↾ 0 ..^ N ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ N ”⟩
121 120 fveq2d ⊢ φ → lastS ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N = lastS ⁡ M seq str F ↾ 0 ..^ N ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ N ”⟩
122 fzo0ssnn0 ⊢ 0 ..^ N ⊆ ℕ 0
123 fssres ⊢ M seq str F : ℕ 0 ⟶ S ∧ 0 ..^ N ⊆ ℕ 0 → M seq str F ↾ 0 ..^ N : 0 ..^ N ⟶ S
124 81 122 123 sylancl ⊢ φ → M seq str F ↾ 0 ..^ N : 0 ..^ N ⟶ S
125 iswrdi ⊢ M seq str F ↾ 0 ..^ N : 0 ..^ N ⟶ S → M seq str F ↾ 0 ..^ N ∈ Word S
126 124 125 syl ⊢ φ → M seq str F ↾ 0 ..^ N ∈ Word S
127 elex ⊢ M seq str F ↾ 0 ..^ N ∈ Word S → M seq str F ↾ 0 ..^ N ∈ V
128 126 127 syl ⊢ φ → M seq str F ↾ 0 ..^ N ∈ V
129 eluznn0 ⊢ M ∈ ℕ 0 ∧ N ∈ ℤ ≥ M → N ∈ ℕ 0
130 41 5 129 syl2anc ⊢ φ → N ∈ ℕ 0
131 1 81 130 subiwrdlen ⊢ φ → M seq str F ↾ 0 ..^ N = N
132 131 5 eqeltrd ⊢ φ → M seq str F ↾ 0 ..^ N ∈ ℤ ≥ M
133 elpreima ⊢ . Fn V → M seq str F ↾ 0 ..^ N ∈ . -1 ℤ ≥ M ↔ M seq str F ↾ 0 ..^ N ∈ V ∧ M seq str F ↾ 0 ..^ N ∈ ℤ ≥ M
134 95 96 133 mp2b ⊢ M seq str F ↾ 0 ..^ N ∈ . -1 ℤ ≥ M ↔ M seq str F ↾ 0 ..^ N ∈ V ∧ M seq str F ↾ 0 ..^ N ∈ ℤ ≥ M
135 128 132 134 sylanbrc ⊢ φ → M seq str F ↾ 0 ..^ N ∈ . -1 ℤ ≥ M
136 126 135 elind ⊢ φ → M seq str F ↾ 0 ..^ N ∈ Word S ∩ . -1 ℤ ≥ M
137 136 3 eleqtrrdi ⊢ φ → M seq str F ↾ 0 ..^ N ∈ W
138 4 137 ffvelcdmd ⊢ φ → F ⁡ M seq str F ↾ 0 ..^ N ∈ S
139 lswccats1 ⊢ M seq str F ↾ 0 ..^ N ∈ Word S ∧ F ⁡ M seq str F ↾ 0 ..^ N ∈ S → lastS ⁡ M seq str F ↾ 0 ..^ N ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ N ”⟩ = F ⁡ M seq str F ↾ 0 ..^ N
140 126 138 139 syl2anc ⊢ φ → lastS ⁡ M seq str F ↾ 0 ..^ N ++ ⟨“ F ⁡ M seq str F ↾ 0 ..^ N ”⟩ = F ⁡ M seq str F ↾ 0 ..^ N
141 6 121 140 3eqtrd ⊢ φ → M seq str F ⁡ N = F ⁡ M seq str F ↾ 0 ..^ N