Step | Hyp | Ref
| Expression |
1 | | cspc 29945 |
. 2
class
Lambda |
2 | | vt |
. . 3
setvar ๐ก |
3 | | chba 29903 |
. . . 4
class
โ |
4 | | cmap 8772 |
. . . 4
class
โm |
5 | 3, 3, 4 | co 7362 |
. . 3
class ( โ
โm โ) |
6 | 2 | cv 1541 |
. . . . . . 7
class ๐ก |
7 | | vx |
. . . . . . . . 9
setvar ๐ฅ |
8 | 7 | cv 1541 |
. . . . . . . 8
class ๐ฅ |
9 | | cid 5535 |
. . . . . . . . 9
class
I |
10 | 9, 3 | cres 5640 |
. . . . . . . 8
class ( I
โพ โ) |
11 | | chot 29923 |
. . . . . . . 8
class
ยทop |
12 | 8, 10, 11 | co 7362 |
. . . . . . 7
class (๐ฅ ยทop (
I โพ โ)) |
13 | | chod 29924 |
. . . . . . 7
class
โop |
14 | 6, 12, 13 | co 7362 |
. . . . . 6
class (๐ก โop (๐ฅ ยทop (
I โพ โ))) |
15 | 3, 3, 14 | wf1 6498 |
. . . . 5
wff (๐ก โop (๐ฅ ยทop (
I โพ โ))): โโ1-1โ โ |
16 | 15 | wn 3 |
. . . 4
wff ยฌ
(๐ก โop
(๐ฅ
ยทop ( I โพ โ))): โโ1-1โ โ |
17 | | cc 11056 |
. . . 4
class
โ |
18 | 16, 7, 17 | crab 3410 |
. . 3
class {๐ฅ โ โ โฃ ยฌ
(๐ก โop
(๐ฅ
ยทop ( I โพ โ))): โโ1-1โ โ} |
19 | 2, 5, 18 | cmpt 5193 |
. 2
class (๐ก โ ( โ
โm โ) โฆ {๐ฅ โ โ โฃ ยฌ (๐ก โop (๐ฅ ยทop (
I โพ โ))): โโ1-1โ โ}) |
20 | 1, 19 | wceq 1542 |
1
wff Lambda =
(๐ก โ ( โ
โm โ) โฆ {๐ฅ โ โ โฃ ยฌ (๐ก โop (๐ฅ ยทop (
I โพ โ))): โโ1-1โ โ}) |