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	⊢ 𝒫 { ∅ , { ∅ } } = ( { ∅ , { ∅ } } ∪ { { { ∅ } } , { ∅ , { ∅ } } } )