Step | Hyp | Ref
| Expression |
1 | | cleo 29942 |
. 2
class
โคop |
2 | | vu |
. . . . . . 7
setvar ๐ข |
3 | 2 | cv 1541 |
. . . . . 6
class ๐ข |
4 | | vt |
. . . . . . 7
setvar ๐ก |
5 | 4 | cv 1541 |
. . . . . 6
class ๐ก |
6 | | chod 29924 |
. . . . . 6
class
โop |
7 | 3, 5, 6 | co 7358 |
. . . . 5
class (๐ข โop ๐ก) |
8 | | cho 29934 |
. . . . 5
class
HrmOp |
9 | 7, 8 | wcel 2107 |
. . . 4
wff (๐ข โop ๐ก) โ HrmOp |
10 | | cc0 11056 |
. . . . . 6
class
0 |
11 | | vx |
. . . . . . . . 9
setvar ๐ฅ |
12 | 11 | cv 1541 |
. . . . . . . 8
class ๐ฅ |
13 | 12, 7 | cfv 6497 |
. . . . . . 7
class ((๐ข โop ๐ก)โ๐ฅ) |
14 | | csp 29906 |
. . . . . . 7
class
ยทih |
15 | 13, 12, 14 | co 7358 |
. . . . . 6
class (((๐ข โop ๐ก)โ๐ฅ) ยทih ๐ฅ) |
16 | | cle 11195 |
. . . . . 6
class
โค |
17 | 10, 15, 16 | wbr 5106 |
. . . . 5
wff 0 โค
(((๐ข โop
๐ก)โ๐ฅ) ยทih ๐ฅ) |
18 | | chba 29903 |
. . . . 5
class
โ |
19 | 17, 11, 18 | wral 3061 |
. . . 4
wff
โ๐ฅ โ
โ 0 โค (((๐ข
โop ๐ก)โ๐ฅ) ยทih ๐ฅ) |
20 | 9, 19 | wa 397 |
. . 3
wff ((๐ข โop ๐ก) โ HrmOp โง
โ๐ฅ โ โ 0
โค (((๐ข
โop ๐ก)โ๐ฅ) ยทih ๐ฅ)) |
21 | 20, 4, 2 | copab 5168 |
. 2
class
{โจ๐ก, ๐ขโฉ โฃ ((๐ข โop ๐ก) โ HrmOp โง
โ๐ฅ โ โ 0
โค (((๐ข
โop ๐ก)โ๐ฅ) ยทih ๐ฅ))} |
22 | 1, 21 | wceq 1542 |
1
wff
โคop = {โจ๐ก, ๐ขโฉ โฃ ((๐ข โop ๐ก) โ HrmOp โง โ๐ฅ โ โ 0 โค (((๐ข โop ๐ก)โ๐ฅ) ยทih ๐ฅ))} |