Step | Hyp | Ref
| Expression |
1 | | sseqval.1 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ V) |
2 | | sseqval.2 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Word 𝑆) |
3 | | sseqval.3 |
. . . 4
⊢ 𝑊 = (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀)))) |
4 | | sseqval.4 |
. . . 4
⊢ (𝜑 → 𝐹:𝑊⟶𝑆) |
5 | 1, 2, 3, 4 | sseqval 30578 |
. . 3
⊢ (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))) |
6 | 5 | fveq1d 6231 |
. 2
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = ((𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))‘𝑁)) |
7 | | wrdfn 13351 |
. . . 4
⊢ (𝑀 ∈ Word 𝑆 → 𝑀 Fn (0..^(#‘𝑀))) |
8 | 2, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀 Fn (0..^(#‘𝑀))) |
9 | | fvex 6239 |
. . . . . 6
⊢ (𝑥‘((#‘𝑥) − 1)) ∈
V |
10 | | df-lsw 13332 |
. . . . . 6
⊢ lastS =
(𝑥 ∈ V ↦ (𝑥‘((#‘𝑥) − 1))) |
11 | 9, 10 | fnmpti 6060 |
. . . . 5
⊢ lastS Fn
V |
12 | 11 | a1i 11 |
. . . 4
⊢ (𝜑 → lastS Fn
V) |
13 | | lencl 13356 |
. . . . . . 7
⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈
ℕ0) |
14 | 2, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘𝑀) ∈
ℕ0) |
15 | 14 | nn0zd 11518 |
. . . . 5
⊢ (𝜑 → (#‘𝑀) ∈ ℤ) |
16 | | seqfn 12853 |
. . . . 5
⊢
((#‘𝑀) ∈
ℤ → seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(#‘𝑀))) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ (𝜑 → seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(#‘𝑀))) |
18 | | ssv 3658 |
. . . . 5
⊢ ran
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ⊆
V |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → ran seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ⊆
V) |
20 | | fnco 6037 |
. . . 4
⊢ (( lastS
Fn V ∧ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(#‘𝑀)) ∧ ran seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ⊆ V)
→ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) Fn
(ℤ≥‘(#‘𝑀))) |
21 | 12, 17, 19, 20 | syl3anc 1366 |
. . 3
⊢ (𝜑 → ( lastS ∘
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) Fn
(ℤ≥‘(#‘𝑀))) |
22 | | fzouzdisj 12543 |
. . . 4
⊢
((0..^(#‘𝑀))
∩ (ℤ≥‘(#‘𝑀))) = ∅ |
23 | 22 | a1i 11 |
. . 3
⊢ (𝜑 → ((0..^(#‘𝑀)) ∩
(ℤ≥‘(#‘𝑀))) = ∅) |
24 | | sseqfv2.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘(#‘𝑀))) |
25 | | fvun2 6309 |
. . 3
⊢ ((𝑀 Fn (0..^(#‘𝑀)) ∧ ( lastS ∘
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) Fn
(ℤ≥‘(#‘𝑀)) ∧ (((0..^(#‘𝑀)) ∩
(ℤ≥‘(#‘𝑀))) = ∅ ∧ 𝑁 ∈
(ℤ≥‘(#‘𝑀)))) → ((𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))‘𝑁) = (( lastS ∘
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁)) |
26 | 8, 21, 23, 24, 25 | syl112anc 1370 |
. 2
⊢ (𝜑 → ((𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))‘𝑁) = (( lastS ∘
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁)) |
27 | | fnfun 6026 |
. . . 4
⊢
(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(#‘𝑀)) → Fun seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) |
28 | 17, 27 | syl 17 |
. . 3
⊢ (𝜑 → Fun seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) |
29 | | fvexd 6241 |
. . . . . 6
⊢ (𝜑 → ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘(#‘𝑀)) ∈ V) |
30 | | ovexd 6720 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))𝑏) ∈ V) |
31 | | eqid 2651 |
. . . . . 6
⊢
(ℤ≥‘(#‘𝑀)) =
(ℤ≥‘(#‘𝑀)) |
32 | | fvexd 6241 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘((#‘𝑀) + 1))) → ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘𝑎) ∈ V) |
33 | 29, 30, 31, 15, 32 | seqf2 12860 |
. . . . 5
⊢ (𝜑 → seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})):(ℤ≥‘(#‘𝑀))⟶V) |
34 | | fdm 6089 |
. . . . 5
⊢
(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})):(ℤ≥‘(#‘𝑀))⟶V → dom seq(#‘𝑀)((𝑥 ∈ V, 𝑦
∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})) =
(ℤ≥‘(#‘𝑀))) |
35 | 33, 34 | syl 17 |
. . . 4
⊢ (𝜑 → dom seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) =
(ℤ≥‘(#‘𝑀))) |
36 | 24, 35 | eleqtrrd 2733 |
. . 3
⊢ (𝜑 → 𝑁 ∈ dom seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) |
37 | | fvco 6313 |
. . 3
⊢ ((Fun
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ∧ 𝑁 ∈ dom seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) → ((
lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁) = ( lastS
‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |
38 | 28, 36, 37 | syl2anc 694 |
. 2
⊢ (𝜑 → (( lastS ∘
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁) = ( lastS
‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |
39 | 6, 26, 38 | 3eqtrd 2689 |
1
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |