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→ 𝒫 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	⊢ 𝒫 V = V
5		foeq3	⊢ ( 𝒫 V = V → ( I : V –onto→ 𝒫 V ↔ I : V –onto→ V ) )
6	4 5	ax-mp	⊢ ( I : V –onto→ 𝒫 V ↔ I : V –onto→ V )
7	3 6	mpbir	⊢ I : V –onto→ 𝒫 V