Detailed syntax breakdown of Definition df-nmoo
| Step | Hyp | Ref
| Expression |
| 1 | | cnmoo 30760 |
. 2
class
normOpOLD |
| 2 | | vu |
. . 3
setvar 𝑢 |
| 3 | | vw |
. . 3
setvar 𝑤 |
| 4 | | cnv 30603 |
. . 3
class
NrmCVec |
| 5 | | vt |
. . . 4
setvar 𝑡 |
| 6 | 3 | cv 1539 |
. . . . . 6
class 𝑤 |
| 7 | | cba 30605 |
. . . . . 6
class
BaseSet |
| 8 | 6, 7 | cfv 6561 |
. . . . 5
class
(BaseSet‘𝑤) |
| 9 | 2 | cv 1539 |
. . . . . 6
class 𝑢 |
| 10 | 9, 7 | cfv 6561 |
. . . . 5
class
(BaseSet‘𝑢) |
| 11 | | cmap 8866 |
. . . . 5
class
↑m |
| 12 | 8, 10, 11 | co 7431 |
. . . 4
class
((BaseSet‘𝑤)
↑m (BaseSet‘𝑢)) |
| 13 | | vz |
. . . . . . . . . . 11
setvar 𝑧 |
| 14 | 13 | cv 1539 |
. . . . . . . . . 10
class 𝑧 |
| 15 | | cnmcv 30609 |
. . . . . . . . . . 11
class
normCV |
| 16 | 9, 15 | cfv 6561 |
. . . . . . . . . 10
class
(normCV‘𝑢) |
| 17 | 14, 16 | cfv 6561 |
. . . . . . . . 9
class
((normCV‘𝑢)‘𝑧) |
| 18 | | c1 11156 |
. . . . . . . . 9
class
1 |
| 19 | | cle 11296 |
. . . . . . . . 9
class
≤ |
| 20 | 17, 18, 19 | wbr 5143 |
. . . . . . . 8
wff
((normCV‘𝑢)‘𝑧) ≤ 1 |
| 21 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
| 22 | 21 | cv 1539 |
. . . . . . . . 9
class 𝑥 |
| 23 | 5 | cv 1539 |
. . . . . . . . . . 11
class 𝑡 |
| 24 | 14, 23 | cfv 6561 |
. . . . . . . . . 10
class (𝑡‘𝑧) |
| 25 | 6, 15 | cfv 6561 |
. . . . . . . . . 10
class
(normCV‘𝑤) |
| 26 | 24, 25 | cfv 6561 |
. . . . . . . . 9
class
((normCV‘𝑤)‘(𝑡‘𝑧)) |
| 27 | 22, 26 | wceq 1540 |
. . . . . . . 8
wff 𝑥 =
((normCV‘𝑤)‘(𝑡‘𝑧)) |
| 28 | 20, 27 | wa 395 |
. . . . . . 7
wff
(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧))) |
| 29 | 28, 13, 10 | wrex 3070 |
. . . . . 6
wff
∃𝑧 ∈
(BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧))) |
| 30 | 29, 21 | cab 2714 |
. . . . 5
class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))} |
| 31 | | cxr 11294 |
. . . . 5
class
ℝ* |
| 32 | | clt 11295 |
. . . . 5
class
< |
| 33 | 30, 31, 32 | csup 9480 |
. . . 4
class
sup({𝑥 ∣
∃𝑧 ∈
(BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, <
) |
| 34 | 5, 12, 33 | cmpt 5225 |
. . 3
class (𝑡 ∈ ((BaseSet‘𝑤) ↑m
(BaseSet‘𝑢)) ↦
sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, <
)) |
| 35 | 2, 3, 4, 4, 34 | cmpo 7433 |
. 2
class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m
(BaseSet‘𝑢)) ↦
sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, <
))) |
| 36 | 1, 35 | wceq 1540 |
1
wff
normOpOLD = (𝑢
∈ NrmCVec, 𝑤 ∈
NrmCVec ↦ (𝑡 ∈
((BaseSet‘𝑤)
↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, <
))) |