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