Metamath Proof Explorer

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 ⊢ x | ∃ y x = 𝒫 y ∉ V

Proof

Step Hyp Ref Expression
1 abnex ⊢ ∀ y 𝒫 y ∈ V ∧ y ∈ 𝒫 y → ¬ x | ∃ y x = 𝒫 y ∈ V
2 df-nel ⊢ x | ∃ y x = 𝒫 y ∉ V ↔ ¬ x | ∃ y x = 𝒫 y ∈ V
3 1 2 sylibr ⊢ ∀ y 𝒫 y ∈ V ∧ y ∈ 𝒫 y → x | ∃ y x = 𝒫 y ∉ V
4 vpwex ⊢ 𝒫 y ∈ V
5 vex ⊢ y ∈ V
6 5 pwid ⊢ y ∈ 𝒫 y
7 4 6 pm3.2i ⊢ 𝒫 y ∈ V ∧ y ∈ 𝒫 y
8 3 7 mpg ⊢ x | ∃ y x = 𝒫 y ∉ V