Metamath Proof Explorer


Theorem pwpwpw0

Description: Compute the power set of the power set of the power set of the empty set. (See also pw0 and pwpw0 .) (Contributed by NM, 2-May-2009)

Ref Expression
Assertion pwpwpw0 𝒫 =

Proof

Step Hyp Ref Expression
1 pwpr 𝒫 =