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 29777 |
. . 3
⊢ (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))) |
6 | 5 | fveq1d 6105 |
. 2
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = ((𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))‘𝑁)) |
7 | | wrdfn 13174 |
. . . 4
⊢ (𝑀 ∈ Word 𝑆 → 𝑀 Fn (0..^(#‘𝑀))) |
8 | 2, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀 Fn (0..^(#‘𝑀))) |
9 | | fvex 6113 |
. . . . . 6
⊢ (𝑥‘((#‘𝑥) − 1)) ∈
V |
10 | | df-lsw 13155 |
. . . . . 6
⊢ lastS =
(𝑥 ∈ V ↦ (𝑥‘((#‘𝑥) − 1))) |
11 | 9, 10 | fnmpti 5935 |
. . . . 5
⊢ lastS Fn
V |
12 | 11 | a1i 11 |
. . . 4
⊢ (𝜑 → lastS Fn
V) |
13 | | lencl 13179 |
. . . . . . 7
⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈
ℕ0) |
14 | 2, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘𝑀) ∈
ℕ0) |
15 | 14 | nn0zd 11356 |
. . . . 5
⊢ (𝜑 → (#‘𝑀) ∈ ℤ) |
16 | | seqfn 12675 |
. . . . 5
⊢
((#‘𝑀) ∈
ℤ → seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(#‘𝑀))) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ (𝜑 → seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(#‘𝑀))) |
18 | | ssv 3588 |
. . . . 5
⊢ ran
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ⊆
V |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → ran seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ⊆
V) |
20 | | fnco 5913 |
. . . 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 1318 |
. . 3
⊢ (𝜑 → ( lastS ∘
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) Fn
(ℤ≥‘(#‘𝑀))) |
22 | | fzouzdisj 12373 |
. . . 4
⊢
((0..^(#‘𝑀))
∩ (ℤ≥‘(#‘𝑀))) = ∅ |
23 | 22 | a1i 11 |
. . 3
⊢ (𝜑 → ((0..^(#‘𝑀)) ∩
(ℤ≥‘(#‘𝑀))) = ∅) |
24 | | sseqfv2.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘(#‘𝑀))) |
25 | | fvun2 6180 |
. . 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 1322 |
. 2
⊢ (𝜑 → ((𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))‘𝑁) = (( lastS ∘
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁)) |
27 | | fnfun 5902 |
. . . 4
⊢
(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) Fn
(ℤ≥‘(#‘𝑀)) → Fun seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) |
28 | 17, 27 | syl 17 |
. . 3
⊢ (𝜑 → Fun seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) |
29 | | fvex 6113 |
. . . . . . 7
⊢
((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘(#‘𝑀)) ∈ V |
30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘(#‘𝑀)) ∈ V) |
31 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑥 ++ 〈“(𝐹‘𝑥)”〉) ∈ V |
32 | 31 | rgen2w 2909 |
. . . . . . . . 9
⊢
∀𝑥 ∈ V
∀𝑦 ∈ V (𝑥 ++ 〈“(𝐹‘𝑥)”〉) ∈ V |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ V ∀𝑦 ∈ V (𝑥 ++ 〈“(𝐹‘𝑥)”〉) ∈ V) |
34 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)) = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)) |
35 | 34 | fmpt2 7126 |
. . . . . . . 8
⊢
(∀𝑥 ∈ V
∀𝑦 ∈ V (𝑥 ++ 〈“(𝐹‘𝑥)”〉) ∈ V ↔ (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)):(V ×
V)⟶V) |
36 | 33, 35 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)):(V ×
V)⟶V) |
37 | 36 | fovrnda 6703 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))𝑏) ∈ V) |
38 | | eqid 2610 |
. . . . . 6
⊢
(ℤ≥‘(#‘𝑀)) =
(ℤ≥‘(#‘𝑀)) |
39 | | fvex 6113 |
. . . . . . 7
⊢
((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘𝑎) ∈ V |
40 | 39 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘((#‘𝑀) + 1))) → ((ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})‘𝑎) ∈ V) |
41 | 30, 37, 38, 15, 40 | seqf2 12682 |
. . . . 5
⊢ (𝜑 → seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})):(ℤ≥‘(#‘𝑀))⟶V) |
42 | | fdm 5964 |
. . . . 5
⊢
(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})):(ℤ≥‘(#‘𝑀))⟶V → dom seq(#‘𝑀)((𝑥 ∈ V, 𝑦
∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})) =
(ℤ≥‘(#‘𝑀))) |
43 | 41, 42 | syl 17 |
. . . 4
⊢ (𝜑 → dom seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) =
(ℤ≥‘(#‘𝑀))) |
44 | 24, 43 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → 𝑁 ∈ dom seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) |
45 | | fvco 6184 |
. . 3
⊢ ((Fun
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ∧ 𝑁 ∈ dom seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) → ((
lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁) = ( lastS
‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |
46 | 28, 44, 45 | syl2anc 691 |
. 2
⊢ (𝜑 → (( lastS ∘
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))‘𝑁) = ( lastS
‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |
47 | 6, 26, 46 | 3eqtrd 2648 |
1
⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))‘𝑁))) |