Detailed syntax breakdown of Definition df-sseq
Step | Hyp | Ref
| Expression |
1 | | csseq 30445 |
. 2
class
seqstr |
2 | | vm |
. . 3
setvar 𝑚 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cvv 3200 |
. . 3
class
V |
5 | 2 | cv 1482 |
. . . 4
class 𝑚 |
6 | | clsw 13292 |
. . . . 5
class
lastS |
7 | | vx |
. . . . . . 7
setvar 𝑥 |
8 | | vy |
. . . . . . 7
setvar 𝑦 |
9 | 7 | cv 1482 |
. . . . . . . 8
class 𝑥 |
10 | 3 | cv 1482 |
. . . . . . . . . 10
class 𝑓 |
11 | 9, 10 | cfv 5888 |
. . . . . . . . 9
class (𝑓‘𝑥) |
12 | 11 | cs1 13294 |
. . . . . . . 8
class
〈“(𝑓‘𝑥)”〉 |
13 | | cconcat 13293 |
. . . . . . . 8
class
++ |
14 | 9, 12, 13 | co 6650 |
. . . . . . 7
class (𝑥 ++ 〈“(𝑓‘𝑥)”〉) |
15 | 7, 8, 4, 4, 14 | cmpt2 6652 |
. . . . . 6
class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)) |
16 | | cn0 11292 |
. . . . . . 7
class
ℕ0 |
17 | 5, 10 | cfv 5888 |
. . . . . . . . . 10
class (𝑓‘𝑚) |
18 | 17 | cs1 13294 |
. . . . . . . . 9
class
〈“(𝑓‘𝑚)”〉 |
19 | 5, 18, 13 | co 6650 |
. . . . . . . 8
class (𝑚 ++ 〈“(𝑓‘𝑚)”〉) |
20 | 19 | csn 4177 |
. . . . . . 7
class {(𝑚 ++ 〈“(𝑓‘𝑚)”〉)} |
21 | 16, 20 | cxp 5112 |
. . . . . 6
class
(ℕ0 × {(𝑚 ++ 〈“(𝑓‘𝑚)”〉)}) |
22 | | chash 13117 |
. . . . . . 7
class
# |
23 | 5, 22 | cfv 5888 |
. . . . . 6
class
(#‘𝑚) |
24 | 15, 21, 23 | cseq 12801 |
. . . . 5
class
seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)})) |
25 | 6, 24 | ccom 5118 |
. . . 4
class ( lastS
∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)}))) |
26 | 5, 25 | cun 3572 |
. . 3
class (𝑚 ∪ ( lastS ∘
seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)})))) |
27 | 2, 3, 4, 4, 26 | cmpt2 6652 |
. 2
class (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)}))))) |
28 | 1, 27 | wceq 1483 |
1
wff
seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ ( lastS ∘ seq(#‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)}))))) |