Description: The power class of the universe is the universe. Exercise 4.12(d) of Mendelson p. 235.
The collection of all classes is of course larger than _V , which is the collection of all sets. But ~PV , being a class, cannot contain proper classes, so ~P V is actually no larger than _V . This fact is exploited in ncanth . (Contributed by NM, 14-Sep-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | pwv | |- ~P _V = _V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssv | |- x C_ _V |
|
2 | velpw | |- ( x e. ~P _V <-> x C_ _V ) |
|
3 | 1 2 | mpbir | |- x e. ~P _V |
4 | vex | |- x e. _V |
|
5 | 3 4 | 2th | |- ( x e. ~P _V <-> x e. _V ) |
6 | 5 | eqriv | |- ~P _V = _V |