Step | Hyp | Ref
| Expression |
1 | | sseqval.1 |
. . 3
⊢ (𝜑 → 𝑆 ∈ V) |
2 | | sseqval.2 |
. . 3
⊢ (𝜑 → 𝑀 ∈ Word 𝑆) |
3 | | sseqval.3 |
. . 3
⊢ 𝑊 = (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀)))) |
4 | | sseqval.4 |
. . 3
⊢ (𝜑 → 𝐹:𝑊⟶𝑆) |
5 | | sseqfv2.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘(#‘𝑀))) |
6 | 1, 2, 3, 4, 5 | sseqfv2 29783 |
. 2
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |
7 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑖 = (#‘𝑀) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(#‘𝑀))) |
8 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑖 = (#‘𝑀) → (0..^𝑖) = (0..^(#‘𝑀))) |
9 | 8 | reseq2d 5317 |
. . . . . . . 8
⊢ (𝑖 = (#‘𝑀) → ((𝑀seqstr𝐹) ↾ (0..^𝑖)) = ((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀)))) |
10 | 9 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑖 = (#‘𝑀) → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))))) |
11 | 10 | s1eqd 13234 |
. . . . . . . 8
⊢ (𝑖 = (#‘𝑀) → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉 = 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))))”〉) |
12 | 9, 11 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑖 = (#‘𝑀) → (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))))”〉)) |
13 | 7, 12 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑖 = (#‘𝑀) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(#‘𝑀)) = (((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))))”〉))) |
14 | 13 | imbi2d 329 |
. . . . 5
⊢ (𝑖 = (#‘𝑀) → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(#‘𝑀)) = (((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))))”〉)))) |
15 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑖 = 𝑛 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)) |
16 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (0..^𝑖) = (0..^𝑛)) |
17 | 16 | reseq2d 5317 |
. . . . . . . 8
⊢ (𝑖 = 𝑛 → ((𝑀seqstr𝐹) ↾ (0..^𝑖)) = ((𝑀seqstr𝐹) ↾ (0..^𝑛))) |
18 | 17 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))) |
19 | 18 | s1eqd 13234 |
. . . . . . . 8
⊢ (𝑖 = 𝑛 → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉 = 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉) |
20 | 17, 19 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑖 = 𝑛 → (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) |
21 | 15, 20 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑖 = 𝑛 → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉))) |
22 | 21 | imbi2d 329 |
. . . . 5
⊢ (𝑖 = 𝑛 → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)))) |
23 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑖 = (𝑛 + 1) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1))) |
24 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑖 = (𝑛 + 1) → (0..^𝑖) = (0..^(𝑛 + 1))) |
25 | 24 | reseq2d 5317 |
. . . . . . . 8
⊢ (𝑖 = (𝑛 + 1) → ((𝑀seqstr𝐹) ↾ (0..^𝑖)) = ((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1)))) |
26 | 25 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑖 = (𝑛 + 1) → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))) |
27 | 26 | s1eqd 13234 |
. . . . . . . 8
⊢ (𝑖 = (𝑛 + 1) → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉 = 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉) |
28 | 25, 27 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑖 = (𝑛 + 1) → (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)) |
29 | 23, 28 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑖 = (𝑛 + 1) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉))) |
30 | 29 | imbi2d 329 |
. . . . 5
⊢ (𝑖 = (𝑛 + 1) → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)))) |
31 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑖 = 𝑁 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁)) |
32 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑖 = 𝑁 → (0..^𝑖) = (0..^𝑁)) |
33 | 32 | reseq2d 5317 |
. . . . . . . 8
⊢ (𝑖 = 𝑁 → ((𝑀seqstr𝐹) ↾ (0..^𝑖)) = ((𝑀seqstr𝐹) ↾ (0..^𝑁))) |
34 | 33 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑖 = 𝑁 → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))) |
35 | 34 | s1eqd 13234 |
. . . . . . . 8
⊢ (𝑖 = 𝑁 → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉 = 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉) |
36 | 33, 35 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑖 = 𝑁 → (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)) |
37 | 31, 36 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑖 = 𝑁 → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉))) |
38 | 37 | imbi2d 329 |
. . . . 5
⊢ (𝑖 = 𝑁 → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)))) |
39 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V |
40 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈
ℕ0) |
41 | 2, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝑀) ∈
ℕ0) |
42 | | fvconst2g 6372 |
. . . . . . . 8
⊢ (((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V ∧
(#‘𝑀) ∈
ℕ0) → ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(#‘𝑀)) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
43 | 39, 41, 42 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘(#‘𝑀)) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
44 | 40 | nn0zd 11356 |
. . . . . . . 8
⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈ ℤ) |
45 | | seq1 12676 |
. . . . . . . 8
⊢
((#‘𝑀) ∈
ℤ → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(#‘𝑀)) = ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘(#‘𝑀))) |
46 | 2, 44, 45 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(#‘𝑀)) = ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘(#‘𝑀))) |
47 | 1, 2, 3, 4 | sseqfres 29782 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))) = 𝑀) |
48 | 47 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀)))) = (𝐹‘𝑀)) |
49 | 48 | s1eqd 13234 |
. . . . . . . 8
⊢ (𝜑 → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))))”〉 = 〈“(𝐹‘𝑀)”〉) |
50 | 47, 49 | oveq12d 6567 |
. . . . . . 7
⊢ (𝜑 → (((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))))”〉) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
51 | 43, 46, 50 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(#‘𝑀)) = (((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))))”〉)) |
52 | 51 | a1i 11 |
. . . . 5
⊢
((#‘𝑀) ∈
ℤ → (𝜑 →
(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(#‘𝑀)) = (((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(#‘𝑀))))”〉))) |
53 | | seqp1 12678 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘(#‘𝑀)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) |
54 | 53 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) |
55 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → 𝑥 = 𝑎) |
56 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎)) |
57 | 56 | s1eqd 13234 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → 〈“(𝐹‘𝑥)”〉 = 〈“(𝐹‘𝑎)”〉) |
58 | 55, 57 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑥 ++ 〈“(𝐹‘𝑥)”〉) = (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
59 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑏 → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) = (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
60 | 58, 59 | cbvmpt2v 6633 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
61 | 60 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ++ 〈“(𝐹‘𝑎)”〉))) |
62 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∧ 𝑏 = ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) → 𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∧ 𝑏 = ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) → (𝐹‘𝑎) = (𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))) |
64 | 63 | s1eqd 13234 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∧ 𝑏 = ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) → 〈“(𝐹‘𝑎)”〉 = 〈“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉) |
65 | 62, 64 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∧ 𝑏 = ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉)) |
66 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∈ V |
67 | 66 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∈ V) |
68 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)) ∈ V |
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)) ∈ V) |
70 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉) ∈
V |
71 | 70 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉) ∈
V) |
72 | 61, 65, 67, 69, 71 | ovmpt2d 6686 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1))) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉)) |
73 | 54, 72 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉)) |
74 | 73 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉)) |
75 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → 𝑆 ∈ V) |
76 | 2 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → 𝑀 ∈ Word 𝑆) |
77 | 4 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → 𝐹:𝑊⟶𝑆) |
78 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → 𝑛 ∈
(ℤ≥‘(#‘𝑀))) |
79 | 75, 76, 3, 77, 78 | sseqfv2 29783 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((𝑀seqstr𝐹)‘𝑛) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))) |
80 | 79 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → ((𝑀seqstr𝐹)‘𝑛) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))) |
81 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) |
82 | 81 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → ( lastS
‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)) = ( lastS ‘(((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉))) |
83 | 1, 2, 3, 4 | sseqf 29781 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀seqstr𝐹):ℕ0⟶𝑆) |
84 | | fzo0ssnn0 12415 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0..^𝑛) ⊆
ℕ0 |
85 | | fssres 5983 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀seqstr𝐹):ℕ0⟶𝑆 ∧ (0..^𝑛) ⊆ ℕ0) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆) |
86 | 83, 84, 85 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆) |
87 | | iswrdi 13164 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆 → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆) |
90 | | elex 3185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆 → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ V) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ V) |
92 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → (𝑀seqstr𝐹):ℕ0⟶𝑆) |
93 | | eluznn0 11633 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝑀) ∈
ℕ0 ∧ 𝑛
∈ (ℤ≥‘(#‘𝑀))) → 𝑛 ∈ ℕ0) |
94 | 41, 93 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → 𝑛 ∈ ℕ0) |
95 | 75, 92, 94 | subiwrdlen 29775 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → (#‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) = 𝑛) |
96 | 95, 78 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → (#‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈
(ℤ≥‘(#‘𝑀))) |
97 | | hashf 12987 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
#:V⟶(ℕ0 ∪ {+∞}) |
98 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(#:V⟶(ℕ0 ∪ {+∞}) → # Fn
V) |
99 | | elpreima 6245 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (# Fn V
→ (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ V ∧ (#‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈
(ℤ≥‘(#‘𝑀))))) |
100 | 97, 98, 99 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ V ∧ (#‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈
(ℤ≥‘(#‘𝑀)))) |
101 | 91, 96, 100 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ (◡# “
(ℤ≥‘(#‘𝑀)))) |
102 | 89, 101 | elind 3760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀))))) |
103 | 102, 3 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ 𝑊) |
104 | 77, 103 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈ 𝑆) |
105 | | lswccats1 13263 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆 ∧ (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈ 𝑆) → ( lastS ‘(((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))) |
106 | 89, 104, 105 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ( lastS ‘(((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → ( lastS
‘(((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))) |
108 | 80, 82, 107 | 3eqtrrd 2649 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) = ((𝑀seqstr𝐹)‘𝑛)) |
109 | 108 | s1eqd 13234 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉 = 〈“((𝑀seqstr𝐹)‘𝑛)”〉) |
110 | 109 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“((𝑀seqstr𝐹)‘𝑛)”〉)) |
111 | 75, 92, 94 | iwrdsplit 29776 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“((𝑀seqstr𝐹)‘𝑛)”〉)) |
112 | 111 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → ((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“((𝑀seqstr𝐹)‘𝑛)”〉)) |
113 | 110, 81, 112 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = ((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1)))) |
114 | 113 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))) |
115 | 114 | s1eqd 13234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → 〈“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉 =
〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉) |
116 | 113, 115 | oveq12d 6567 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)) |
117 | 74, 116 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)) |
118 | 117 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(#‘𝑀))) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉))) |
119 | 118 | expcom 450 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘(#‘𝑀)) → (𝜑 → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)))) |
120 | 119 | a2d 29 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘(#‘𝑀)) → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)))) |
121 | 14, 22, 30, 38, 52, 120 | uzind4 11622 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘(#‘𝑀)) → (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉))) |
122 | 5, 121 | mpcom 37 |
. . 3
⊢ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)) |
123 | 122 | fveq2d 6107 |
. 2
⊢ (𝜑 → ( lastS
‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁)) = ( lastS ‘(((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉))) |
124 | | fzo0ssnn0 12415 |
. . . . 5
⊢
(0..^𝑁) ⊆
ℕ0 |
125 | | fssres 5983 |
. . . . 5
⊢ (((𝑀seqstr𝐹):ℕ0⟶𝑆 ∧ (0..^𝑁) ⊆ ℕ0) →
((𝑀seqstr𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆) |
126 | 83, 124, 125 | sylancl 693 |
. . . 4
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆) |
127 | | iswrdi 13164 |
. . . 4
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆) |
128 | 126, 127 | syl 17 |
. . 3
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆) |
129 | | elex 3185 |
. . . . . . . 8
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ V) |
130 | 128, 129 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ V) |
131 | | eluznn0 11633 |
. . . . . . . . . 10
⊢
(((#‘𝑀) ∈
ℕ0 ∧ 𝑁
∈ (ℤ≥‘(#‘𝑀))) → 𝑁 ∈
ℕ0) |
132 | 41, 5, 131 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
133 | 1, 83, 132 | subiwrdlen 29775 |
. . . . . . . 8
⊢ (𝜑 → (#‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) = 𝑁) |
134 | 133, 5 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝜑 → (#‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈
(ℤ≥‘(#‘𝑀))) |
135 | | elpreima 6245 |
. . . . . . . 8
⊢ (# Fn V
→ (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ V ∧ (#‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈
(ℤ≥‘(#‘𝑀))))) |
136 | 97, 98, 135 | mp2b 10 |
. . . . . . 7
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ V ∧ (#‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈
(ℤ≥‘(#‘𝑀)))) |
137 | 130, 134,
136 | sylanbrc 695 |
. . . . . 6
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ (◡# “
(ℤ≥‘(#‘𝑀)))) |
138 | 128, 137 | elind 3760 |
. . . . 5
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀))))) |
139 | 138, 3 | syl6eleqr 2699 |
. . . 4
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ 𝑊) |
140 | 4, 139 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈ 𝑆) |
141 | | lswccats1 13263 |
. . 3
⊢ ((((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆 ∧ (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈ 𝑆) → ( lastS ‘(((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))) |
142 | 128, 140,
141 | syl2anc 691 |
. 2
⊢ (𝜑 → ( lastS ‘(((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))) |
143 | 6, 123, 142 | 3eqtrd 2648 |
1
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))) |