Step | Hyp | Ref
| Expression |
1 | | cado 29726 |
. 2
class
adjโ |
2 | | chba 29690 |
. . . . 5
class
โ |
3 | | vt |
. . . . . 6
setvar ๐ก |
4 | 3 | cv 1540 |
. . . . 5
class ๐ก |
5 | 2, 2, 4 | wf 6489 |
. . . 4
wff ๐ก: โโถ
โ |
6 | | vu |
. . . . . 6
setvar ๐ข |
7 | 6 | cv 1540 |
. . . . 5
class ๐ข |
8 | 2, 2, 7 | wf 6489 |
. . . 4
wff ๐ข: โโถ
โ |
9 | | vx |
. . . . . . . . . 10
setvar ๐ฅ |
10 | 9 | cv 1540 |
. . . . . . . . 9
class ๐ฅ |
11 | 10, 4 | cfv 6493 |
. . . . . . . 8
class (๐กโ๐ฅ) |
12 | | vy |
. . . . . . . . 9
setvar ๐ฆ |
13 | 12 | cv 1540 |
. . . . . . . 8
class ๐ฆ |
14 | | csp 29693 |
. . . . . . . 8
class
ยทih |
15 | 11, 13, 14 | co 7351 |
. . . . . . 7
class ((๐กโ๐ฅ) ยทih ๐ฆ) |
16 | 13, 7 | cfv 6493 |
. . . . . . . 8
class (๐ขโ๐ฆ) |
17 | 10, 16, 14 | co 7351 |
. . . . . . 7
class (๐ฅ
ยทih (๐ขโ๐ฆ)) |
18 | 15, 17 | wceq 1541 |
. . . . . 6
wff ((๐กโ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)) |
19 | 18, 12, 2 | wral 3062 |
. . . . 5
wff
โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)) |
20 | 19, 9, 2 | wral 3062 |
. . . 4
wff
โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)) |
21 | 5, 8, 20 | w3a 1087 |
. . 3
wff (๐ก: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ))) |
22 | 21, 3, 6 | copab 5165 |
. 2
class
{โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง
๐ข: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)))} |
23 | 1, 22 | wceq 1541 |
1
wff
adjโ = {โจ๐ก, ๐ขโฉ โฃ (๐ก: โโถ โ โง ๐ข: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐กโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐ขโ๐ฆ)))} |