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

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 ⊢ 𝒫 ∅ ∅ = ∅ ∅ ∪ ∅ ∅ ∅