Detailed syntax breakdown of Definition df-homul
Step | Hyp | Ref
| Expression |
1 | | chot 29309 |
. 2
class
·op |
2 | | vf |
. . 3
setvar 𝑓 |
3 | | vg |
. . 3
setvar 𝑔 |
4 | | cc 10879 |
. . 3
class
ℂ |
5 | | chba 29289 |
. . . 4
class
ℋ |
6 | | cmap 8602 |
. . . 4
class
↑m |
7 | 5, 5, 6 | co 7267 |
. . 3
class ( ℋ
↑m ℋ) |
8 | | vx |
. . . 4
setvar 𝑥 |
9 | 2 | cv 1538 |
. . . . 5
class 𝑓 |
10 | 8 | cv 1538 |
. . . . . 6
class 𝑥 |
11 | 3 | cv 1538 |
. . . . . 6
class 𝑔 |
12 | 10, 11 | cfv 6426 |
. . . . 5
class (𝑔‘𝑥) |
13 | | csm 29291 |
. . . . 5
class
·ℎ |
14 | 9, 12, 13 | co 7267 |
. . . 4
class (𝑓
·ℎ (𝑔‘𝑥)) |
15 | 8, 5, 14 | cmpt 5156 |
. . 3
class (𝑥 ∈ ℋ ↦ (𝑓
·ℎ (𝑔‘𝑥))) |
16 | 2, 3, 4, 7, 15 | cmpo 7269 |
. 2
class (𝑓 ∈ ℂ, 𝑔 ∈ ( ℋ
↑m ℋ) ↦ (𝑥 ∈ ℋ ↦ (𝑓 ·ℎ (𝑔‘𝑥)))) |
17 | 1, 16 | wceq 1539 |
1
wff
·op = (𝑓 ∈ ℂ, 𝑔 ∈ ( ℋ ↑m ℋ)
↦ (𝑥 ∈ ℋ
↦ (𝑓
·ℎ (𝑔‘𝑥)))) |