Detailed syntax breakdown of Definition df-hmop
Step | Hyp | Ref
| Expression |
1 | | cho 29321 |
. 2
class
HrmOp |
2 | | vx |
. . . . . . . 8
setvar 𝑥 |
3 | 2 | cv 1538 |
. . . . . . 7
class 𝑥 |
4 | | vy |
. . . . . . . . 9
setvar 𝑦 |
5 | 4 | cv 1538 |
. . . . . . . 8
class 𝑦 |
6 | | vt |
. . . . . . . . 9
setvar 𝑡 |
7 | 6 | cv 1538 |
. . . . . . . 8
class 𝑡 |
8 | 5, 7 | cfv 6437 |
. . . . . . 7
class (𝑡‘𝑦) |
9 | | csp 29293 |
. . . . . . 7
class
·ih |
10 | 3, 8, 9 | co 7284 |
. . . . . 6
class (𝑥
·ih (𝑡‘𝑦)) |
11 | 3, 7 | cfv 6437 |
. . . . . . 7
class (𝑡‘𝑥) |
12 | 11, 5, 9 | co 7284 |
. . . . . 6
class ((𝑡‘𝑥) ·ih 𝑦) |
13 | 10, 12 | wceq 1539 |
. . . . 5
wff (𝑥
·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) |
14 | | chba 29290 |
. . . . 5
class
ℋ |
15 | 13, 4, 14 | wral 3065 |
. . . 4
wff
∀𝑦 ∈
ℋ (𝑥
·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) |
16 | 15, 2, 14 | wral 3065 |
. . 3
wff
∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦) |
17 | | cmap 8624 |
. . . 4
class
↑m |
18 | 14, 14, 17 | co 7284 |
. . 3
class ( ℋ
↑m ℋ) |
19 | 16, 6, 18 | crab 3069 |
. 2
class {𝑡 ∈ ( ℋ
↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)} |
20 | 1, 19 | wceq 1539 |
1
wff HrmOp =
{𝑡 ∈ ( ℋ
↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)} |