Theorem ncanth 7114

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

This failure comes from a limitation of the collection principle (which is necessary to avoid Russell's paradox ru 3773): 𝒫 V, 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 𝒫 V (see pwv 4837). See also the remark in ru 3773 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.)

Assertion

Ref	Expression
ncanth	⊢ I :V–onto→𝒫 V

Proof of Theorem ncanth

Step	Hyp	Ref	Expression
1		f1ovi 6655	. . 3 ⊢ I :V–1-1-onto→V
2		f1ofo 6624	. . 3 ⊢ ( I :V–1-1-onto→V → I :V–onto→V)
3	1, 2	ax-mp 5	. 2 ⊢ I :V–onto→V
4		pwv 4837	. . 3 ⊢ 𝒫 V = V
5		foeq3 6590	. . 3 ⊢ (𝒫 V = V → ( I :V–onto→𝒫 V ↔ I :V–onto→V))
6	4, 5	ax-mp 5	. 2 ⊢ ( I :V–onto→𝒫 V ↔ I :V–onto→V)
7	3, 6	mpbir 233	1 ⊢ I :V–onto→𝒫 V

Syntax hints:   ↔ wb 208   = wceq 1537  Vcvv 3496  𝒫 cpw 4541   I cid 5461  –onto→wfo 6355  –1-1-onto→wf1o 6356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364

This theorem is referenced by: (None)