Metamath Proof Explorer


Theorem canth

Description: No set A is equinumerous to its power set (Cantor's theorem), i.e., no function can map A onto its power set. Compare Theorem 6B(b) of Enderton p. 132. For the equinumerosity version, see canth2 . Note that A must be a set: this theorem does not hold when A is too large to be a set; see ncanth for a counterexample. (Use nex if you want the form -. E. f f : A -onto-> ~P A .) (Contributed by NM, 7-Aug-1994) (Proof shortened by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypothesis canth.1 𝐴 ∈ V
Assertion canth ¬ 𝐹 : 𝐴onto→ 𝒫 𝐴

Proof

Step Hyp Ref Expression
1 canth.1 𝐴 ∈ V
2 ssrab2 { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ⊆ 𝐴
3 1 2 elpwi2 { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ∈ 𝒫 𝐴
4 forn ( 𝐹 : 𝐴onto→ 𝒫 𝐴 → ran 𝐹 = 𝒫 𝐴 )
5 3 4 eleqtrrid ( 𝐹 : 𝐴onto→ 𝒫 𝐴 → { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ∈ ran 𝐹 )
6 id ( 𝑥 = 𝑦𝑥 = 𝑦 )
7 fveq2 ( 𝑥 = 𝑦 → ( 𝐹𝑥 ) = ( 𝐹𝑦 ) )
8 6 7 eleq12d ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( 𝐹𝑥 ) ↔ 𝑦 ∈ ( 𝐹𝑦 ) ) )
9 8 notbid ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ ( 𝐹𝑥 ) ↔ ¬ 𝑦 ∈ ( 𝐹𝑦 ) ) )
10 9 elrab ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ↔ ( 𝑦𝐴 ∧ ¬ 𝑦 ∈ ( 𝐹𝑦 ) ) )
11 10 baibr ( 𝑦𝐴 → ( ¬ 𝑦 ∈ ( 𝐹𝑦 ) ↔ 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ) )
12 nbbn ( ( ¬ 𝑦 ∈ ( 𝐹𝑦 ) ↔ 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ) ↔ ¬ ( 𝑦 ∈ ( 𝐹𝑦 ) ↔ 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ) )
13 11 12 sylib ( 𝑦𝐴 → ¬ ( 𝑦 ∈ ( 𝐹𝑦 ) ↔ 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ) )
14 eleq2 ( ( 𝐹𝑦 ) = { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } → ( 𝑦 ∈ ( 𝐹𝑦 ) ↔ 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ) )
15 13 14 nsyl ( 𝑦𝐴 → ¬ ( 𝐹𝑦 ) = { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } )
16 15 nrex ¬ ∃ 𝑦𝐴 ( 𝐹𝑦 ) = { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) }
17 fofn ( 𝐹 : 𝐴onto→ 𝒫 𝐴𝐹 Fn 𝐴 )
18 fvelrnb ( 𝐹 Fn 𝐴 → ( { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ∈ ran 𝐹 ↔ ∃ 𝑦𝐴 ( 𝐹𝑦 ) = { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ) )
19 17 18 syl ( 𝐹 : 𝐴onto→ 𝒫 𝐴 → ( { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ∈ ran 𝐹 ↔ ∃ 𝑦𝐴 ( 𝐹𝑦 ) = { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ) )
20 16 19 mtbiri ( 𝐹 : 𝐴onto→ 𝒫 𝐴 → ¬ { 𝑥𝐴 ∣ ¬ 𝑥 ∈ ( 𝐹𝑥 ) } ∈ ran 𝐹 )
21 5 20 pm2.65i ¬ 𝐹 : 𝐴onto→ 𝒫 𝐴