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 
|- ~P { (/) , { (/) } } = ( { (/) , { (/) } } u. { { { (/) } } , { (/) , { (/) } } } )

Proof

Step Hyp Ref Expression
1 pwpr 
 |-  ~P { (/) , { (/) } } = ( { (/) , { (/) } } u. { { { (/) } } , { (/) , { (/) } } } )