MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ncanth Structured version   Visualization version   GIF version

Theorem ncanth 6385
Description: Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc 4623). Specifically, the identity function maps the universe onto its power class. Compare canth 6384 that works for sets. See also the remark in ru 3305 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
StepHypRef Expression
1 f1ovi 5970 . . 3 I :V–1-1-onto→V
2 pwv 4269 . . . 4 𝒫 V = V
3 f1oeq3 5925 . . . 4 (𝒫 V = V → ( I :V–1-1-onto→𝒫 V ↔ I :V–1-1-onto→V))
42, 3ax-mp 5 . . 3 ( I :V–1-1-onto→𝒫 V ↔ I :V–1-1-onto→V)
51, 4mpbir 219 . 2 I :V–1-1-onto→𝒫 V
6 f1ofo 5940 . 2 ( I :V–1-1-onto→𝒫 V → I :V–onto→𝒫 V)
75, 6ax-mp 5 1 I :V–onto→𝒫 V
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  Vcvv 3077  𝒫 cpw 4011   I cid 4842  ontowfo 5687  1-1-ontowf1o 5688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-op 4035  df-br 4482  df-opab 4542  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator