This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwnss

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

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

Step	Hyp	Ref	Expression
1		rru	$⊢ \neg \{x \in A \| \neg x \in x\} \in A$
2		ssel	$⊢ 𝒫 A \subseteq A \to (\{x \in A \| \neg x \in x\} \in 𝒫 A \to \{x \in A \| \neg x \in x\} \in A)$
3	1 2	mtoi	$⊢ 𝒫 A \subseteq A \to \neg \{x \in A \| \neg x \in x\} \in 𝒫 A$
4		rabelpw	$⊢ A \in V \to \{x \in A \| \neg x \in x\} \in 𝒫 A$
5	3 4	nsyl3	$⊢ A \in V \to \neg 𝒫 A \subseteq A$