Theorem canthwdom

Description: Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 , equivalent to canth ). (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	canthwdom	$$⊢\neg 𝒫A{\preccurlyeq }^{*}A$$

Proof

Step	Hyp	Ref	Expression
1		0elpw	$$⊢\varnothing \in 𝒫A$$
2		ne0i	$$⊢\varnothing \in 𝒫A\to 𝒫A\ne \varnothing$$
3	1 2	mp1i	$$⊢𝒫A{\preccurlyeq }^{*}A\to 𝒫A\ne \varnothing$$
4		brwdomn0	$$⊢𝒫A\ne \varnothing \to \left(𝒫A{\preccurlyeq }^{*}A\leftrightarrow \exists ff:A\underset{onto}{⟶}𝒫A\right)$$
5	3 4	syl	$$⊢𝒫A{\preccurlyeq }^{*}A\to \left(𝒫A{\preccurlyeq }^{*}A\leftrightarrow \exists ff:A\underset{onto}{⟶}𝒫A\right)$$
6	5	ibi	$$⊢𝒫A{\preccurlyeq }^{*}A\to \exists ff:A\underset{onto}{⟶}𝒫A$$
7		relwdom	$$⊢\mathrm{Rel}{\preccurlyeq }^{*}$$
8	7	brrelex2i	$$⊢𝒫A{\preccurlyeq }^{*}A\to A\in \mathrm{V}$$
9		foeq2	$$⊢x=A\to \left(f:x\underset{onto}{⟶}𝒫x\leftrightarrow f:A\underset{onto}{⟶}𝒫x\right)$$
10		pweq	$$⊢x=A\to 𝒫x=𝒫A$$
11		foeq3	$$⊢𝒫x=𝒫A\to \left(f:A\underset{onto}{⟶}𝒫x\leftrightarrow f:A\underset{onto}{⟶}𝒫A\right)$$
12	10 11	syl	$$⊢x=A\to \left(f:A\underset{onto}{⟶}𝒫x\leftrightarrow f:A\underset{onto}{⟶}𝒫A\right)$$
13	9 12	bitrd	$$⊢x=A\to \left(f:x\underset{onto}{⟶}𝒫x\leftrightarrow f:A\underset{onto}{⟶}𝒫A\right)$$
14	13	notbid	$$⊢x=A\to \left(\neg f:x\underset{onto}{⟶}𝒫x\leftrightarrow \neg f:A\underset{onto}{⟶}𝒫A\right)$$
15		vex	$$⊢x\in \mathrm{V}$$
16	15	canth	$$⊢\neg f:x\underset{onto}{⟶}𝒫x$$
17	14 16	vtoclg	$$⊢A\in \mathrm{V}\to \neg f:A\underset{onto}{⟶}𝒫A$$
18	8 17	syl	$$⊢𝒫A{\preccurlyeq }^{*}A\to \neg f:A\underset{onto}{⟶}𝒫A$$
19	18	nexdv	$$⊢𝒫A{\preccurlyeq }^{*}A\to \neg \exists ff:A\underset{onto}{⟶}𝒫A$$
20	6 19	pm2.65i	$$⊢\neg 𝒫A{\preccurlyeq }^{*}A$$