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	$$⊢A\in \mathrm{V}$$
Assertion	canth	$$⊢\neg F:A\underset{onto}{⟶}𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		canth.1	$$⊢A\in \mathrm{V}$$
2		ssrab2	$$⊢\left\{x\in A|\neg x\in F\left(x\right)\right\}\subseteq A$$
3	1 2	elpwi2	$$⊢\left\{x\in A|\neg x\in F\left(x\right)\right\}\in 𝒫A$$
4		forn	$$⊢F:A\underset{onto}{⟶}𝒫A\to \mathrm{ran}F=𝒫A$$
5	3 4	eleqtrrid	$$⊢F:A\underset{onto}{⟶}𝒫A\to \left\{x\in A|\neg x\in F\left(x\right)\right\}\in \mathrm{ran}F$$
6		id	$$⊢x=y\to x=y$$
7		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
8	6 7	eleq12d	$$⊢x=y\to \left(x\in F\left(x\right)\leftrightarrow y\in F\left(y\right)\right)$$
9	8	notbid	$$⊢x=y\to \left(\neg x\in F\left(x\right)\leftrightarrow \neg y\in F\left(y\right)\right)$$
10	9	elrab	$$⊢y\in \left\{x\in A|\neg x\in F\left(x\right)\right\}\leftrightarrow \left(y\in A\wedge \neg y\in F\left(y\right)\right)$$
11	10	baibr	$$⊢y\in A\to \left(\neg y\in F\left(y\right)\leftrightarrow y\in \left\{x\in A|\neg x\in F\left(x\right)\right\}\right)$$
12		nbbn	$$⊢\left(\neg y\in F\left(y\right)\leftrightarrow y\in \left\{x\in A|\neg x\in F\left(x\right)\right\}\right)\leftrightarrow \neg \left(y\in F\left(y\right)\leftrightarrow y\in \left\{x\in A|\neg x\in F\left(x\right)\right\}\right)$$
13	11 12	sylib	$$⊢y\in A\to \neg \left(y\in F\left(y\right)\leftrightarrow y\in \left\{x\in A|\neg x\in F\left(x\right)\right\}\right)$$
14		eleq2	$$⊢F\left(y\right)=\left\{x\in A|\neg x\in F\left(x\right)\right\}\to \left(y\in F\left(y\right)\leftrightarrow y\in \left\{x\in A|\neg x\in F\left(x\right)\right\}\right)$$
15	13 14	nsyl	$$⊢y\in A\to \neg F\left(y\right)=\left\{x\in A|\neg x\in F\left(x\right)\right\}$$
16	15	nrex	$$⊢\neg \exists y\in AF\left(y\right)=\left\{x\in A|\neg x\in F\left(x\right)\right\}$$
17		fofn	$$⊢F:A\underset{onto}{⟶}𝒫A\to FFnA$$
18		fvelrnb	$$⊢FFnA\to \left(\left\{x\in A|\neg x\in F\left(x\right)\right\}\in \mathrm{ran}F\leftrightarrow \exists y\in AF\left(y\right)=\left\{x\in A|\neg x\in F\left(x\right)\right\}\right)$$
19	17 18	syl	$$⊢F:A\underset{onto}{⟶}𝒫A\to \left(\left\{x\in A|\neg x\in F\left(x\right)\right\}\in \mathrm{ran}F\leftrightarrow \exists y\in AF\left(y\right)=\left\{x\in A|\neg x\in F\left(x\right)\right\}\right)$$
20	16 19	mtbiri	$$⊢F:A\underset{onto}{⟶}𝒫A\to \neg \left\{x\in A|\neg x\in F\left(x\right)\right\}\in \mathrm{ran}F$$
21	5 20	pm2.65i	$$⊢\neg F:A\underset{onto}{⟶}𝒫A$$