Step | Hyp | Ref
| Expression |
1 | | cho 29721 |
. 2
class
HrmOp |
2 | | vx |
. . . . . . . 8
setvar ๐ฅ |
3 | 2 | cv 1540 |
. . . . . . 7
class ๐ฅ |
4 | | vy |
. . . . . . . . 9
setvar ๐ฆ |
5 | 4 | cv 1540 |
. . . . . . . 8
class ๐ฆ |
6 | | vt |
. . . . . . . . 9
setvar ๐ก |
7 | 6 | cv 1540 |
. . . . . . . 8
class ๐ก |
8 | 5, 7 | cfv 6493 |
. . . . . . 7
class (๐กโ๐ฆ) |
9 | | csp 29693 |
. . . . . . 7
class
ยทih |
10 | 3, 8, 9 | co 7351 |
. . . . . 6
class (๐ฅ
ยทih (๐กโ๐ฆ)) |
11 | 3, 7 | cfv 6493 |
. . . . . . 7
class (๐กโ๐ฅ) |
12 | 11, 5, 9 | co 7351 |
. . . . . 6
class ((๐กโ๐ฅ) ยทih ๐ฆ) |
13 | 10, 12 | wceq 1541 |
. . . . 5
wff (๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) |
14 | | chba 29690 |
. . . . 5
class
โ |
15 | 13, 4, 14 | wral 3062 |
. . . 4
wff
โ๐ฆ โ
โ (๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) |
16 | 15, 2, 14 | wral 3062 |
. . 3
wff
โ๐ฅ โ
โ โ๐ฆ โ
โ (๐ฅ
ยทih (๐กโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ) |
17 | | cmap 8723 |
. . . 4
class
โm |
18 | 14, 14, 17 | co 7351 |
. . 3
class ( โ
โm โ) |
19 | 16, 6, 18 | crab 3405 |
. 2
class {๐ก โ ( โ
โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐กโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)} |
20 | 1, 19 | wceq 1541 |
1
wff HrmOp =
{๐ก โ ( โ
โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ (๐ฅ ยทih (๐กโ๐ฆ)) = ((๐กโ๐ฅ) ยทih ๐ฆ)} |