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

Proof

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