Theorem ncanth 6323

Description: Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc 4574). Specifically, the identity function maps the universe onto its power class. Compare canth 6322 that works for sets. See also the remark in ru 3290 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.)

Assertion

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

Proof of Theorem ncanth

Step	Hyp	Ref	Expression
1		f1ovi 5911	. . 3 ⊢ I :V–1-1-onto→V
2		pwv 4227	. . . 4 ⊢ 𝒫 V = V
3		f1oeq3 5866	. . . 4 ⊢ (𝒫 V = V → ( I :V–1-1-onto→𝒫 V ↔ I :V–1-1-onto→V))
4	2, 3	ax-mp 5	. . 3 ⊢ ( I :V–1-1-onto→𝒫 V ↔ I :V–1-1-onto→V)
5	1, 4	mpbir 216	. 2 ⊢ I :V–1-1-onto→𝒫 V
6		f1ofo 5881	. 2 ⊢ ( I :V–1-1-onto→𝒫 V → I :V–onto→𝒫 V)
7	5, 6	ax-mp 5	1 ⊢ I :V–onto→𝒫 V

Syntax hints:   ↔ wb 191   = wceq 1468  Vcvv 3066  𝒫 cpw 3978   I cid 4790  –onto→wfo 5631  –1-1-onto→wf1o 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-op 4002  df-br 4435  df-opab 4494  df-id 4795  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640

This theorem is referenced by: (None)