Theorem 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	⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 = 𝒫 𝑦 } ∉ V

Proof

Step	Hyp	Ref	Expression
1		abnex	⊢ ( ∀ 𝑦 ( 𝒫 𝑦 ∈ V ∧ 𝑦 ∈ 𝒫 𝑦 ) → ¬ { 𝑥 ∣ ∃ 𝑦 𝑥 = 𝒫 𝑦 } ∈ V )
2		df-nel	⊢ ( { 𝑥 ∣ ∃ 𝑦 𝑥 = 𝒫 𝑦 } ∉ V ↔ ¬ { 𝑥 ∣ ∃ 𝑦 𝑥 = 𝒫 𝑦 } ∈ V )
3	1 2	sylibr	⊢ ( ∀ 𝑦 ( 𝒫 𝑦 ∈ V ∧ 𝑦 ∈ 𝒫 𝑦 ) → { 𝑥 ∣ ∃ 𝑦 𝑥 = 𝒫 𝑦 } ∉ V )
4		vpwex	⊢ 𝒫 𝑦 ∈ V
5		vex	⊢ 𝑦 ∈ V
6	5	pwid	⊢ 𝑦 ∈ 𝒫 𝑦
7	4 6	pm3.2i	⊢ ( 𝒫 𝑦 ∈ V ∧ 𝑦 ∈ 𝒫 𝑦 )
8	3 7	mpg	⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 = 𝒫 𝑦 } ∉ V