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 32073 |
. 2
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |
7 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑖 = (♯‘𝑀) →
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(♯‘𝑀))) |
8 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑖 = (♯‘𝑀) → (0..^𝑖) = (0..^(♯‘𝑀))) |
9 | 8 | reseq2d 5851 |
. . . . . . . 8
⊢ (𝑖 = (♯‘𝑀) → ((𝑀seqstr𝐹) ↾ (0..^𝑖)) = ((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀)))) |
10 | 9 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝑖 = (♯‘𝑀) → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))))) |
11 | 10 | s1eqd 14158 |
. . . . . . . 8
⊢ (𝑖 = (♯‘𝑀) → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉 = 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))))”〉) |
12 | 9, 11 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑖 = (♯‘𝑀) → (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))))”〉)) |
13 | 7, 12 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑖 = (♯‘𝑀) →
((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) ↔
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(♯‘𝑀)) = (((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))))”〉))) |
14 | 13 | imbi2d 344 |
. . . . 5
⊢ (𝑖 = (♯‘𝑀) → ((𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉)) ↔ (𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(♯‘𝑀)) = (((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))))”〉)))) |
15 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑖 = 𝑛 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)) |
16 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (0..^𝑖) = (0..^𝑛)) |
17 | 16 | reseq2d 5851 |
. . . . . . . 8
⊢ (𝑖 = 𝑛 → ((𝑀seqstr𝐹) ↾ (0..^𝑖)) = ((𝑀seqstr𝐹) ↾ (0..^𝑛))) |
18 | 17 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))) |
19 | 18 | s1eqd 14158 |
. . . . . . . 8
⊢ (𝑖 = 𝑛 → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉 = 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉) |
20 | 17, 19 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑖 = 𝑛 → (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) |
21 | 15, 20 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑖 = 𝑛 → ((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) ↔
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉))) |
22 | 21 | imbi2d 344 |
. . . . 5
⊢ (𝑖 = 𝑛 → ((𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉)) ↔ (𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)))) |
23 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑖 = (𝑛 + 1) → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1))) |
24 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑖 = (𝑛 + 1) → (0..^𝑖) = (0..^(𝑛 + 1))) |
25 | 24 | reseq2d 5851 |
. . . . . . . 8
⊢ (𝑖 = (𝑛 + 1) → ((𝑀seqstr𝐹) ↾ (0..^𝑖)) = ((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1)))) |
26 | 25 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝑖 = (𝑛 + 1) → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))) |
27 | 26 | s1eqd 14158 |
. . . . . . . 8
⊢ (𝑖 = (𝑛 + 1) → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉 = 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉) |
28 | 25, 27 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑖 = (𝑛 + 1) → (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)) |
29 | 23, 28 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑖 = (𝑛 + 1) → ((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) ↔
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉))) |
30 | 29 | imbi2d 344 |
. . . . 5
⊢ (𝑖 = (𝑛 + 1) → ((𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉)) ↔ (𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)))) |
31 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑖 = 𝑁 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁)) |
32 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑖 = 𝑁 → (0..^𝑖) = (0..^𝑁)) |
33 | 32 | reseq2d 5851 |
. . . . . . . 8
⊢ (𝑖 = 𝑁 → ((𝑀seqstr𝐹) ↾ (0..^𝑖)) = ((𝑀seqstr𝐹) ↾ (0..^𝑁))) |
34 | 33 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝑖 = 𝑁 → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))) |
35 | 34 | s1eqd 14158 |
. . . . . . . 8
⊢ (𝑖 = 𝑁 → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉 = 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉) |
36 | 33, 35 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑖 = 𝑁 → (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)) |
37 | 31, 36 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑖 = 𝑁 → ((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉) ↔
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉))) |
38 | 37 | imbi2d 344 |
. . . . 5
⊢ (𝑖 = 𝑁 → ((𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑖) = (((𝑀seqstr𝐹) ↾ (0..^𝑖)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑖)))”〉)) ↔ (𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)))) |
39 | | ovex 7246 |
. . . . . . . 8
⊢ (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V |
40 | | lencl 14088 |
. . . . . . . . 9
⊢ (𝑀 ∈ Word 𝑆 → (♯‘𝑀) ∈
ℕ0) |
41 | 2, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑀) ∈
ℕ0) |
42 | | fvconst2g 7017 |
. . . . . . . 8
⊢ (((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V ∧
(♯‘𝑀) ∈
ℕ0) → ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(♯‘𝑀)) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
43 | 39, 41, 42 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘(♯‘𝑀)) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
44 | 40 | nn0zd 12280 |
. . . . . . . 8
⊢ (𝑀 ∈ Word 𝑆 → (♯‘𝑀) ∈ ℤ) |
45 | | seq1 13587 |
. . . . . . . 8
⊢
((♯‘𝑀)
∈ ℤ → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(♯‘𝑀)) = ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘(♯‘𝑀))) |
46 | 2, 44, 45 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(♯‘𝑀)) = ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘(♯‘𝑀))) |
47 | 1, 2, 3, 4 | sseqfres 32072 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) = 𝑀) |
48 | 47 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀)))) = (𝐹‘𝑀)) |
49 | 48 | s1eqd 14158 |
. . . . . . . 8
⊢ (𝜑 → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))))”〉 =
〈“(𝐹‘𝑀)”〉) |
50 | 47, 49 | oveq12d 7231 |
. . . . . . 7
⊢ (𝜑 → (((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))))”〉) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
51 | 43, 46, 50 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(♯‘𝑀)) = (((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))))”〉)) |
52 | 51 | a1i 11 |
. . . . 5
⊢
((♯‘𝑀)
∈ ℤ → (𝜑
→ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(♯‘𝑀)) = (((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))))”〉))) |
53 | | seqp1 13589 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘(♯‘𝑀)) → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) =
((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) |
54 | 53 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) =
((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) |
55 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → 𝑥 = 𝑎) |
56 | | fveq2 6717 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎)) |
57 | 56 | s1eqd 14158 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → 〈“(𝐹‘𝑥)”〉 = 〈“(𝐹‘𝑎)”〉) |
58 | 55, 57 | oveq12d 7231 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑥 ++ 〈“(𝐹‘𝑥)”〉) = (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
59 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑏 → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) = (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
60 | 58, 59 | cbvmpov 7306 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
61 | 60 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ++ 〈“(𝐹‘𝑎)”〉))) |
62 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (𝑎 = (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∧ 𝑏 = ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) → 𝑎 = (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)) |
63 | 62 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (𝑎 = (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∧ 𝑏 = ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) → (𝐹‘𝑎) = (𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))) |
64 | 63 | s1eqd 14158 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (𝑎 = (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∧ 𝑏 = ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) → 〈“(𝐹‘𝑎)”〉 = 〈“(𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉) |
65 | 62, 64 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (𝑎 = (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∧ 𝑏 = ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) = ((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉)) |
66 | | fvexd 6732 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ∈ V) |
67 | | fvexd 6732 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1)) ∈ V) |
68 | | ovex 7246 |
. . . . . . . . . . . . 13
⊢
((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉) ∈
V |
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉) ∈
V) |
70 | 61, 65, 66, 67, 69 | ovmpod 7361 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(𝑛 + 1))) = ((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉)) |
71 | 54, 70 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) =
((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉)) |
72 | 71 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) →
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) =
((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) ++ 〈“(𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉)) |
73 | 1 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → 𝑆 ∈ V) |
74 | 2 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → 𝑀 ∈ Word 𝑆) |
75 | 4 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → 𝐹:𝑊⟶𝑆) |
76 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) |
77 | 73, 74, 3, 75, 76 | sseqfv2 32073 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((𝑀seqstr𝐹)‘𝑛) = (lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))) |
78 | 77 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → ((𝑀seqstr𝐹)‘𝑛) = (lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))) |
79 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) →
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) |
80 | 79 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) →
(lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)) = (lastS‘(((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉))) |
81 | 1, 2, 3, 4 | sseqf 32071 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀seqstr𝐹):ℕ0⟶𝑆) |
82 | | fzo0ssnn0 13323 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0..^𝑛) ⊆
ℕ0 |
83 | | fssres 6585 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀seqstr𝐹):ℕ0⟶𝑆 ∧ (0..^𝑛) ⊆ ℕ0) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆) |
84 | 81, 82, 83 | sylancl 589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆) |
85 | | iswrdi 14073 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆 → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆) |
87 | 86 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆) |
88 | | elex 3426 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆 → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ V) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ V) |
90 | 81 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → (𝑀seqstr𝐹):ℕ0⟶𝑆) |
91 | | eluznn0 12513 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((♯‘𝑀)
∈ ℕ0 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → 𝑛 ∈ ℕ0) |
92 | 41, 91 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → 𝑛 ∈ ℕ0) |
93 | 73, 90, 92 | subiwrdlen 32065 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → (♯‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) = 𝑛) |
94 | 93, 76 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → (♯‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈
(ℤ≥‘(♯‘𝑀))) |
95 | | hashf 13904 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
♯:V⟶(ℕ0 ∪ {+∞}) |
96 | | ffn 6545 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(♯:V⟶(ℕ0 ∪ {+∞}) → ♯
Fn V) |
97 | | elpreima 6878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (♯
Fn V → (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ V ∧ (♯‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈
(ℤ≥‘(♯‘𝑀))))) |
98 | 95, 96, 97 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ V ∧ (♯‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈
(ℤ≥‘(♯‘𝑀)))) |
99 | 89, 94, 98 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) |
100 | 87, 99 | elind 4108 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ (Word 𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀))))) |
101 | 100, 3 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ 𝑊) |
102 | 75, 101 | ffvelrnd 6905 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈ 𝑆) |
103 | | lswccats1 14196 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀seqstr𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆 ∧ (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) ∈ 𝑆) → (lastS‘(((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))) |
104 | 87, 102, 103 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → (lastS‘(((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))) |
105 | 104 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) →
(lastS‘(((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))) |
106 | 78, 80, 105 | 3eqtrrd 2782 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛))) = ((𝑀seqstr𝐹)‘𝑛)) |
107 | 106 | s1eqd 14158 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉 = 〈“((𝑀seqstr𝐹)‘𝑛)”〉) |
108 | 107 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“((𝑀seqstr𝐹)‘𝑛)”〉)) |
109 | 73, 90, 92 | iwrdsplit 32066 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“((𝑀seqstr𝐹)‘𝑛)”〉)) |
110 | 109 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → ((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“((𝑀seqstr𝐹)‘𝑛)”〉)) |
111 | 108, 79, 110 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) →
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = ((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1)))) |
112 | 111 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → (𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))) |
113 | 112 | s1eqd 14158 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) → 〈“(𝐹‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛))”〉 =
〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉) |
114 | 111, 113 | oveq12d 7231 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (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 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) ∧ (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉)) →
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)) |
116 | 115 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈
(ℤ≥‘(♯‘𝑀))) → ((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉) →
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉))) |
117 | 116 | expcom 417 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘(♯‘𝑀)) → (𝜑 → ((seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑛) = (((𝑀seqstr𝐹) ↾ (0..^𝑛)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑛)))”〉) →
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘(𝑛 + 1)) = (((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^(𝑛 + 1))))”〉)))) |
118 | 117 | a2d 29 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘(♯‘𝑀)) → ((𝜑 → (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 12502 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘(♯‘𝑀)) → (𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉))) |
120 | 5, 119 | mpcom 38 |
. . 3
⊢ (𝜑 → (seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁) = (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)) |
121 | 120 | fveq2d 6721 |
. 2
⊢ (𝜑 →
(lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁)) = (lastS‘(((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉))) |
122 | | fzo0ssnn0 13323 |
. . . . 5
⊢
(0..^𝑁) ⊆
ℕ0 |
123 | | fssres 6585 |
. . . . 5
⊢ (((𝑀seqstr𝐹):ℕ0⟶𝑆 ∧ (0..^𝑁) ⊆ ℕ0) →
((𝑀seqstr𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆) |
124 | 81, 122, 123 | sylancl 589 |
. . . 4
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆) |
125 | | iswrdi 14073 |
. . . 4
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆) |
126 | 124, 125 | syl 17 |
. . 3
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆) |
127 | | elex 3426 |
. . . . . . . 8
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ V) |
128 | 126, 127 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ V) |
129 | | eluznn0 12513 |
. . . . . . . . . 10
⊢
(((♯‘𝑀)
∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(♯‘𝑀))) → 𝑁 ∈
ℕ0) |
130 | 41, 5, 129 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
131 | 1, 81, 130 | subiwrdlen 32065 |
. . . . . . . 8
⊢ (𝜑 → (♯‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) = 𝑁) |
132 | 131, 5 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → (♯‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈
(ℤ≥‘(♯‘𝑀))) |
133 | | elpreima 6878 |
. . . . . . . 8
⊢ (♯
Fn V → (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ V ∧ (♯‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈
(ℤ≥‘(♯‘𝑀))))) |
134 | 95, 96, 133 | mp2b 10 |
. . . . . . 7
⊢ (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ (((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ V ∧ (♯‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈
(ℤ≥‘(♯‘𝑀)))) |
135 | 128, 132,
134 | sylanbrc 586 |
. . . . . 6
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) |
136 | 126, 135 | elind 4108 |
. . . . 5
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ (Word 𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀))))) |
137 | 136, 3 | eleqtrrdi 2849 |
. . . 4
⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ 𝑊) |
138 | 4, 137 | ffvelrnd 6905 |
. . 3
⊢ (𝜑 → (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈ 𝑆) |
139 | | lswccats1 14196 |
. . 3
⊢ ((((𝑀seqstr𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆 ∧ (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁))) ∈ 𝑆) → (lastS‘(((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))) |
140 | 126, 138,
139 | syl2anc 587 |
. 2
⊢ (𝜑 → (lastS‘(((𝑀seqstr𝐹) ↾ (0..^𝑁)) ++ 〈“(𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))”〉)) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))) |
141 | 6, 121, 140 | 3eqtrd 2781 |
1
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁)))) |