Detailed syntax breakdown of Definition df-nmop
Step | Hyp | Ref
| Expression |
1 | | cnop 28374 |
. 2
class
normop |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | chba 28348 |
. . . 4
class
ℋ |
4 | | cmap 8140 |
. . . 4
class
↑𝑚 |
5 | 3, 3, 4 | co 6922 |
. . 3
class ( ℋ
↑𝑚 ℋ) |
6 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
7 | 6 | cv 1600 |
. . . . . . . . 9
class 𝑧 |
8 | | cno 28352 |
. . . . . . . . 9
class
normℎ |
9 | 7, 8 | cfv 6135 |
. . . . . . . 8
class
(normℎ‘𝑧) |
10 | | c1 10273 |
. . . . . . . 8
class
1 |
11 | | cle 10412 |
. . . . . . . 8
class
≤ |
12 | 9, 10, 11 | wbr 4886 |
. . . . . . 7
wff
(normℎ‘𝑧) ≤ 1 |
13 | | vx |
. . . . . . . . 9
setvar 𝑥 |
14 | 13 | cv 1600 |
. . . . . . . 8
class 𝑥 |
15 | 2 | cv 1600 |
. . . . . . . . . 10
class 𝑡 |
16 | 7, 15 | cfv 6135 |
. . . . . . . . 9
class (𝑡‘𝑧) |
17 | 16, 8 | cfv 6135 |
. . . . . . . 8
class
(normℎ‘(𝑡‘𝑧)) |
18 | 14, 17 | wceq 1601 |
. . . . . . 7
wff 𝑥 =
(normℎ‘(𝑡‘𝑧)) |
19 | 12, 18 | wa 386 |
. . . . . 6
wff
((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧))) |
20 | 19, 6, 3 | wrex 3091 |
. . . . 5
wff
∃𝑧 ∈
ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧))) |
21 | 20, 13 | cab 2763 |
. . . 4
class {𝑥 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))} |
22 | | cxr 10410 |
. . . 4
class
ℝ* |
23 | | clt 10411 |
. . . 4
class
< |
24 | 21, 22, 23 | csup 8634 |
. . 3
class
sup({𝑥 ∣
∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, <
) |
25 | 2, 5, 24 | cmpt 4965 |
. 2
class (𝑡 ∈ ( ℋ
↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, <
)) |
26 | 1, 25 | wceq 1601 |
1
wff
normop = (𝑡 ∈ ( ℋ ↑𝑚
ℋ) ↦ sup({𝑥
∣ ∃𝑧 ∈
ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, <
)) |