Step | Hyp | Ref
| Expression |
1 | | cwpointsN 38662 |
. 2
class
WAtoms |
2 | | vk |
. . 3
setvar π |
3 | | cvv 3473 |
. . 3
class
V |
4 | | vd |
. . . 4
setvar π |
5 | 2 | cv 1540 |
. . . . 5
class π |
6 | | catm 37938 |
. . . . 5
class
Atoms |
7 | 5, 6 | cfv 6532 |
. . . 4
class
(Atomsβπ) |
8 | 4 | cv 1540 |
. . . . . . 7
class π |
9 | 8 | csn 4622 |
. . . . . 6
class {π} |
10 | | cpolN 38578 |
. . . . . . 7
class
β₯π |
11 | 5, 10 | cfv 6532 |
. . . . . 6
class
(β₯πβπ) |
12 | 9, 11 | cfv 6532 |
. . . . 5
class
((β₯πβπ)β{π}) |
13 | 7, 12 | cdif 3941 |
. . . 4
class
((Atomsβπ)
β ((β₯πβπ)β{π})) |
14 | 4, 7, 13 | cmpt 5224 |
. . 3
class (π β (Atomsβπ) β¦ ((Atomsβπ) β
((β₯πβπ)β{π}))) |
15 | 2, 3, 14 | cmpt 5224 |
. 2
class (π β V β¦ (π β (Atomsβπ) β¦ ((Atomsβπ) β
((β₯πβπ)β{π})))) |
16 | 1, 15 | wceq 1541 |
1
wff WAtoms =
(π β V β¦ (π β (Atomsβπ) β¦ ((Atomsβπ) β
((β₯πβπ)β{π})))) |