Step | Hyp | Ref
| Expression |
1 | | coe 8412 |
. 2
class
โo |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | vy |
. . 3
setvar ๐ฆ |
4 | | con0 6318 |
. . 3
class
On |
5 | 2 | cv 1541 |
. . . . 5
class ๐ฅ |
6 | | c0 4283 |
. . . . 5
class
โ
|
7 | 5, 6 | wceq 1542 |
. . . 4
wff ๐ฅ = โ
|
8 | | c1o 8406 |
. . . . 5
class
1o |
9 | 3 | cv 1541 |
. . . . 5
class ๐ฆ |
10 | 8, 9 | cdif 3908 |
. . . 4
class
(1o โ ๐ฆ) |
11 | | vz |
. . . . . . 7
setvar ๐ง |
12 | | cvv 3446 |
. . . . . . 7
class
V |
13 | 11 | cv 1541 |
. . . . . . . 8
class ๐ง |
14 | | comu 8411 |
. . . . . . . 8
class
ยทo |
15 | 13, 5, 14 | co 7358 |
. . . . . . 7
class (๐ง ยทo ๐ฅ) |
16 | 11, 12, 15 | cmpt 5189 |
. . . . . 6
class (๐ง โ V โฆ (๐ง ยทo ๐ฅ)) |
17 | 16, 8 | crdg 8356 |
. . . . 5
class
rec((๐ง โ V
โฆ (๐ง
ยทo ๐ฅ)),
1o) |
18 | 9, 17 | cfv 6497 |
. . . 4
class
(rec((๐ง โ V
โฆ (๐ง
ยทo ๐ฅ)),
1o)โ๐ฆ) |
19 | 7, 10, 18 | cif 4487 |
. . 3
class if(๐ฅ = โ
, (1o
โ ๐ฆ), (rec((๐ง โ V โฆ (๐ง ยทo ๐ฅ)), 1o)โ๐ฆ)) |
20 | 2, 3, 4, 4, 19 | cmpo 7360 |
. 2
class (๐ฅ โ On, ๐ฆ โ On โฆ if(๐ฅ = โ
, (1o โ ๐ฆ), (rec((๐ง โ V โฆ (๐ง ยทo ๐ฅ)), 1o)โ๐ฆ))) |
21 | 1, 20 | wceq 1542 |
1
wff
โo = (๐ฅ
โ On, ๐ฆ โ On
โฆ if(๐ฅ = โ
,
(1o โ ๐ฆ),
(rec((๐ง โ V โฆ
(๐ง ยทo
๐ฅ)),
1o)โ๐ฆ))) |