Theorem 2pwne

Description: No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008)

	Ref	Expression
Assertion	2pwne	$$⊢A\in V\to 𝒫𝒫A\ne A$$

Proof

Step	Hyp	Ref	Expression
1		sdomirr	$$⊢\neg 𝒫𝒫A\prec 𝒫𝒫A$$
2		canth2g	$$⊢A\in V\to A\prec 𝒫A$$
3		pwexg	$$⊢A\in V\to 𝒫A\in \mathrm{V}$$
4		canth2g	$$⊢𝒫A\in \mathrm{V}\to 𝒫A\prec 𝒫𝒫A$$
5	3 4	syl	$$⊢A\in V\to 𝒫A\prec 𝒫𝒫A$$
6		sdomtr	$$⊢\left(A\prec 𝒫A\wedge 𝒫A\prec 𝒫𝒫A\right)\to A\prec 𝒫𝒫A$$
7	2 5 6	syl2anc	$$⊢A\in V\to A\prec 𝒫𝒫A$$
8		breq1	$$⊢𝒫𝒫A=A\to \left(𝒫𝒫A\prec 𝒫𝒫A\leftrightarrow A\prec 𝒫𝒫A\right)$$
9	7 8	syl5ibrcom	$$⊢A\in V\to \left(𝒫𝒫A=A\to 𝒫𝒫A\prec 𝒫𝒫A\right)$$
10	1 9	mtoi	$$⊢A\in V\to \neg 𝒫𝒫A=A$$
11	10	neqned	$$⊢A\in V\to 𝒫𝒫A\ne A$$