Theorem ncanth

Description: Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc ). Specifically, the identity function maps the universe onto its power class. Compare canth that works for sets.

This failure comes from a limitation of the collection principle (which is necessary to avoid Russell's paradox ru ): ~PV , being a class, cannot contain proper classes, so it is no larger than V , which is why the identity function "succeeds" in being surjective onto ~P _V (see pwv ). See also the remark in ru about NF, in which Cantor's theorem fails for sets that are "too large". This theorem gives some intuition behind that failure: in NF the universal class is a set, and it equals its own power set. (Contributed by NM, 29-Jun-2004) (Proof shortened by BJ, 29-Dec-2023)

	Ref	Expression
Assertion	ncanth	|- _I : _V -onto-> ~P _V

Proof

Step	Hyp	Ref	Expression
1		f1ovi	|- _I : _V -1-1-onto-> _V
2		f1ofo	|- ( _I : _V -1-1-onto-> _V -> _I : _V -onto-> _V )
3	1 2	ax-mp	|- _I : _V -onto-> _V
4		pwv	|- ~P _V = _V
5		foeq3	|- ( ~P _V = _V -> ( _I : _V -onto-> ~P _V <-> _I : _V -onto-> _V ) )
6	4 5	ax-mp	|- ( _I : _V -onto-> ~P _V <-> _I : _V -onto-> _V )
7	3 6	mpbir	|- _I : _V -onto-> ~P _V