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	$$⊢\mathrm{I}:\mathrm{V}\underset{onto}{⟶}𝒫\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		f1ovi	$$⊢\mathrm{I}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
2		f1ofo	$$⊢\mathrm{I}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\to \mathrm{I}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
3	1 2	ax-mp	$$⊢\mathrm{I}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
4		pwv	$$⊢𝒫\mathrm{V}=\mathrm{V}$$
5		foeq3	$$⊢𝒫\mathrm{V}=\mathrm{V}\to \left(\mathrm{I}:\mathrm{V}\underset{onto}{⟶}𝒫\mathrm{V}\leftrightarrow \mathrm{I}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\right)$$
6	4 5	ax-mp	$$⊢\mathrm{I}:\mathrm{V}\underset{onto}{⟶}𝒫\mathrm{V}\leftrightarrow \mathrm{I}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
7	3 6	mpbir	$$⊢\mathrm{I}:\mathrm{V}\underset{onto}{⟶}𝒫\mathrm{V}$$