Detailed syntax breakdown of Definition df-blo
Step | Hyp | Ref
| Expression |
1 | | cblo 28609 |
. 2
class
BLnOp |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | vw |
. . 3
setvar 𝑤 |
4 | | cnv 28451 |
. . 3
class
NrmCVec |
5 | | vt |
. . . . . . 7
setvar 𝑡 |
6 | 5 | cv 1538 |
. . . . . 6
class 𝑡 |
7 | 2 | cv 1538 |
. . . . . . 7
class 𝑢 |
8 | 3 | cv 1538 |
. . . . . . 7
class 𝑤 |
9 | | cnmoo 28608 |
. . . . . . 7
class
normOpOLD |
10 | 7, 8, 9 | co 7143 |
. . . . . 6
class (𝑢 normOpOLD 𝑤) |
11 | 6, 10 | cfv 6328 |
. . . . 5
class ((𝑢 normOpOLD 𝑤)‘𝑡) |
12 | | cpnf 10695 |
. . . . 5
class
+∞ |
13 | | clt 10698 |
. . . . 5
class
< |
14 | 11, 12, 13 | wbr 5025 |
. . . 4
wff ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞ |
15 | | clno 28607 |
. . . . 5
class
LnOp |
16 | 7, 8, 15 | co 7143 |
. . . 4
class (𝑢 LnOp 𝑤) |
17 | 14, 5, 16 | crab 3072 |
. . 3
class {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞} |
18 | 2, 3, 4, 4, 17 | cmpo 7145 |
. 2
class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞}) |
19 | 1, 18 | wceq 1539 |
1
wff BLnOp =
(𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞}) |