Theorem pwnss

Description: The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	pwnss	$$⊢A\in V\to \neg 𝒫A\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		rru	$$⊢\neg \left\{x\in A|\neg x\in x\right\}\in A$$
2		ssel	$$⊢𝒫A\subseteq A\to \left(\left\{x\in A|\neg x\in x\right\}\in 𝒫A\to \left\{x\in A|\neg x\in x\right\}\in A\right)$$
3	1 2	mtoi	$$⊢𝒫A\subseteq A\to \neg \left\{x\in A|\neg x\in x\right\}\in 𝒫A$$
4		ssrab2	$$⊢\left\{x\in A|\neg x\in x\right\}\subseteq A$$
5		elpw2g	$$⊢A\in V\to \left(\left\{x\in A|\neg x\in x\right\}\in 𝒫A\leftrightarrow \left\{x\in A|\neg x\in x\right\}\subseteq A\right)$$
6	4 5	mpbiri	$$⊢A\in V\to \left\{x\in A|\neg x\in x\right\}\in 𝒫A$$
7	3 6	nsyl3	$$⊢A\in V\to \neg 𝒫A\subseteq A$$