pwnex

Description: The class of all power sets is a proper class. See also snnex . (Contributed by BJ, 2-May-2021)

		Ref	Expression
	Assertion	pwnex	$⊢ \{x \| \exists y x = 𝒫 y\} \notin V$

Step	Hyp	Ref	Expression
1		abnex	$⊢ \forall y (𝒫 y \in V \land y \in 𝒫 y) \to \neg \{x \| \exists y x = 𝒫 y\} \in V$
2		df-nel	$⊢ \{x \| \exists y x = 𝒫 y\} \notin V \leftrightarrow \neg \{x \| \exists y x = 𝒫 y\} \in V$
3	1 2	sylibr	$⊢ \forall y (𝒫 y \in V \land y \in 𝒫 y) \to \{x \| \exists y x = 𝒫 y\} \notin V$
4		vpwex	$⊢ 𝒫 y \in V$
5		vex	$⊢ y \in V$
6	5	pwid	$⊢ y \in 𝒫 y$
7	4 6	pm3.2i	$⊢ (𝒫 y \in V \land y \in 𝒫 y)$
8	3 7	mpg	$⊢ \{x \| \exists y x = 𝒫 y\} \notin V$

Metamath Proof Explorer