This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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→ 𝒫 𝐴