Step | Hyp | Ref
| Expression |
1 | | clpad 32954 |
. 2
class
leftpad |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | vw |
. . 3
setvar 𝑤 |
4 | | cvv 3441 |
. . 3
class
V |
5 | | vl |
. . . 4
setvar 𝑙 |
6 | | cn0 12334 |
. . . 4
class
ℕ0 |
7 | | cc0 10972 |
. . . . . . 7
class
0 |
8 | 5 | cv 1539 |
. . . . . . . 8
class 𝑙 |
9 | 3 | cv 1539 |
. . . . . . . . 9
class 𝑤 |
10 | | chash 14145 |
. . . . . . . . 9
class
♯ |
11 | 9, 10 | cfv 6479 |
. . . . . . . 8
class
(♯‘𝑤) |
12 | | cmin 11306 |
. . . . . . . 8
class
− |
13 | 8, 11, 12 | co 7337 |
. . . . . . 7
class (𝑙 − (♯‘𝑤)) |
14 | | cfzo 13483 |
. . . . . . 7
class
..^ |
15 | 7, 13, 14 | co 7337 |
. . . . . 6
class
(0..^(𝑙 −
(♯‘𝑤))) |
16 | 2 | cv 1539 |
. . . . . . 7
class 𝑐 |
17 | 16 | csn 4573 |
. . . . . 6
class {𝑐} |
18 | 15, 17 | cxp 5618 |
. . . . 5
class
((0..^(𝑙 −
(♯‘𝑤))) ×
{𝑐}) |
19 | | cconcat 14373 |
. . . . 5
class
++ |
20 | 18, 9, 19 | co 7337 |
. . . 4
class
(((0..^(𝑙 −
(♯‘𝑤))) ×
{𝑐}) ++ 𝑤) |
21 | 5, 6, 20 | cmpt 5175 |
. . 3
class (𝑙 ∈ ℕ0
↦ (((0..^(𝑙 −
(♯‘𝑤))) ×
{𝑐}) ++ 𝑤)) |
22 | 2, 3, 4, 4, 21 | cmpo 7339 |
. 2
class (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦
(((0..^(𝑙 −
(♯‘𝑤))) ×
{𝑐}) ++ 𝑤))) |
23 | 1, 22 | wceq 1540 |
1
wff leftpad =
(𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0
↦ (((0..^(𝑙 −
(♯‘𝑤))) ×
{𝑐}) ++ 𝑤))) |