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 31925 |
. . 3
⊢ (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))) |
6 | 5 | fveq1d 6676 |
. 2
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = ((𝑀 ∪ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))‘𝑁)) |
7 | | wrdfn 13969 |
. . . 4
⊢ (𝑀 ∈ Word 𝑆 → 𝑀 Fn (0..^(♯‘𝑀))) |
8 | 2, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀 Fn (0..^(♯‘𝑀))) |
9 | | fvex 6687 |
. . . . . 6
⊢ (𝑥‘((♯‘𝑥) − 1)) ∈
V |
10 | | df-lsw 14004 |
. . . . . 6
⊢ lastS =
(𝑥 ∈ V ↦ (𝑥‘((♯‘𝑥) − 1))) |
11 | 9, 10 | fnmpti 6480 |
. . . . 5
⊢ lastS Fn
V |
12 | 11 | a1i 11 |
. . . 4
⊢ (𝜑 → lastS Fn
V) |
13 | | lencl 13974 |
. . . . . . 7
⊢ (𝑀 ∈ Word 𝑆 → (♯‘𝑀) ∈
ℕ0) |
14 | 2, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑀) ∈
ℕ0) |
15 | 14 | nn0zd 12166 |
. . . . 5
⊢ (𝜑 → (♯‘𝑀) ∈
ℤ) |
16 | | seqfn 13472 |
. . . . 5
⊢
((♯‘𝑀)
∈ ℤ → seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(♯‘𝑀))) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ (𝜑 → seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(♯‘𝑀))) |
18 | | ssv 3901 |
. . . . 5
⊢ ran
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ⊆
V |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → ran
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ⊆
V) |
20 | | fnco 6453 |
. . . 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 1372 |
. . 3
⊢ (𝜑 → (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) Fn
(ℤ≥‘(♯‘𝑀))) |
22 | | fzouzdisj 13164 |
. . . 4
⊢
((0..^(♯‘𝑀)) ∩
(ℤ≥‘(♯‘𝑀))) = ∅ |
23 | 22 | a1i 11 |
. . 3
⊢ (𝜑 → ((0..^(♯‘𝑀)) ∩
(ℤ≥‘(♯‘𝑀))) = ∅) |
24 | | sseqfv2.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘(♯‘𝑀))) |
25 | | fvun2 6760 |
. . 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 1375 |
. 2
⊢ (𝜑 → ((𝑀 ∪ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))‘𝑁) = ((lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁)) |
27 | | fnfun 6438 |
. . . 4
⊢
(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(♯‘𝑀)) → Fun seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) |
28 | 17, 27 | syl 17 |
. . 3
⊢ (𝜑 → Fun
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) |
29 | | fvexd 6689 |
. . . . . 6
⊢ (𝜑 → ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘(♯‘𝑀)) ∈ V) |
30 | | ovexd 7205 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))𝑏) ∈ V) |
31 | | eqid 2738 |
. . . . . 6
⊢
(ℤ≥‘(♯‘𝑀)) =
(ℤ≥‘(♯‘𝑀)) |
32 | | fvexd 6689 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘((♯‘𝑀) + 1))) → ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘𝑎) ∈ V) |
33 | 29, 30, 31, 15, 32 | seqf2 13481 |
. . . . 5
⊢ (𝜑 → seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})):(ℤ≥‘(♯‘𝑀))⟶V) |
34 | 33 | fdmd 6515 |
. . . 4
⊢ (𝜑 → dom
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) =
(ℤ≥‘(♯‘𝑀))) |
35 | 24, 34 | eleqtrrd 2836 |
. . 3
⊢ (𝜑 → 𝑁 ∈ dom seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) |
36 | | fvco 6766 |
. . 3
⊢ ((Fun
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ∧ 𝑁 ∈ dom
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) →
((lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁) =
(lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |
37 | 28, 35, 36 | syl2anc 587 |
. 2
⊢ (𝜑 → ((lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁) =
(lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |
38 | 6, 26, 37 | 3eqtrd 2777 |
1
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |