![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ncanth | Structured version Visualization version GIF version |
Description: Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc 4936). Specifically, the identity function maps the universe onto its power class. Compare canth 6759 that works for sets. See also the remark in ru 3563 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.) |
Ref | Expression |
---|---|
ncanth | ⊢ I :V–onto→𝒫 V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1ovi 6324 | . . 3 ⊢ I :V–1-1-onto→V | |
2 | pwv 4573 | . . . 4 ⊢ 𝒫 V = V | |
3 | f1oeq3 6278 | . . . 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 221 | . 2 ⊢ I :V–1-1-onto→𝒫 V |
6 | f1ofo 6293 | . 2 ⊢ ( I :V–1-1-onto→𝒫 V → I :V–onto→𝒫 V) | |
7 | 5, 6 | ax-mp 5 | 1 ⊢ I :V–onto→𝒫 V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1620 Vcvv 3328 𝒫 cpw 4290 I cid 5161 –onto→wfo 6035 –1-1-onto→wf1o 6036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pr 5043 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ral 3043 df-rex 3044 df-rab 3047 df-v 3330 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-op 4316 df-br 4793 df-opab 4853 df-id 5162 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |