Metamath Proof Explorer

Theorem pwpw0

Description: Compute the power set of the power set of the empty set. (See pw0 for the power set of the empty set.) Theorem 90 of Suppes p. 48. Although this theorem is a special case of pwsn , we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994)

Ref Expression
Assertion pwpw0 
|- ~P { (/) } = { (/) , { (/) } }

Proof

Step Hyp Ref Expression
1 dfss2 
 |-  ( x C_ { (/) } <-> A. y ( y e. x -> y e. { (/) } ) )
2 velsn 
 |-  ( y e. { (/) } <-> y = (/) )
3 2 imbi2i 
 |-  ( ( y e. x -> y e. { (/) } ) <-> ( y e. x -> y = (/) ) )
4 3 albii 
 |-  ( A. y ( y e. x -> y e. { (/) } ) <-> A. y ( y e. x -> y = (/) ) )
5 1 4 bitri 
 |-  ( x C_ { (/) } <-> A. y ( y e. x -> y = (/) ) )
6 neq0 
 |-  ( -. x = (/) <-> E. y y e. x )
7 exintr 
 |-  ( A. y ( y e. x -> y = (/) ) -> ( E. y y e. x -> E. y ( y e. x /\ y = (/) ) ) )
8 6 7 syl5bi 
 |-  ( A. y ( y e. x -> y = (/) ) -> ( -. x = (/) -> E. y ( y e. x /\ y = (/) ) ) )
9 exancom 
 |-  ( E. y ( y e. x /\ y = (/) ) <-> E. y ( y = (/) /\ y e. x ) )
10 dfclel 
 |-  ( (/) e. x <-> E. y ( y = (/) /\ y e. x ) )
11 9 10 bitr4i 
 |-  ( E. y ( y e. x /\ y = (/) ) <-> (/) e. x )
12 snssi 
 |-  ( (/) e. x -> { (/) } C_ x )
13 11 12 sylbi 
 |-  ( E. y ( y e. x /\ y = (/) ) -> { (/) } C_ x )
14 8 13 syl6 
 |-  ( A. y ( y e. x -> y = (/) ) -> ( -. x = (/) -> { (/) } C_ x ) )
15 5 14 sylbi 
 |-  ( x C_ { (/) } -> ( -. x = (/) -> { (/) } C_ x ) )
16 15 anc2li 
 |-  ( x C_ { (/) } -> ( -. x = (/) -> ( x C_ { (/) } /\ { (/) } C_ x ) ) )
17 eqss 
 |-  ( x = { (/) } <-> ( x C_ { (/) } /\ { (/) } C_ x ) )
18 16 17 syl6ibr 
 |-  ( x C_ { (/) } -> ( -. x = (/) -> x = { (/) } ) )
19 18 orrd 
 |-  ( x C_ { (/) } -> ( x = (/) \/ x = { (/) } ) )
20 0ss 
 |-  (/) C_ { (/) }
21 sseq1 
 |-  ( x = (/) -> ( x C_ { (/) } <-> (/) C_ { (/) } ) )
22 20 21 mpbiri 
 |-  ( x = (/) -> x C_ { (/) } )
23 eqimss 
 |-  ( x = { (/) } -> x C_ { (/) } )
24 22 23 jaoi 
 |-  ( ( x = (/) \/ x = { (/) } ) -> x C_ { (/) } )
25 19 24 impbii 
 |-  ( x C_ { (/) } <-> ( x = (/) \/ x = { (/) } ) )
26 25 abbii 
 |-  { x | x C_ { (/) } } = { x | ( x = (/) \/ x = { (/) } ) }
27 df-pw 
 |-  ~P { (/) } = { x | x C_ { (/) } }
28 dfpr2 
 |-  { (/) , { (/) } } = { x | ( x = (/) \/ x = { (/) } ) }
29 26 27 28 3eqtr4i 
 |-  ~P { (/) } = { (/) , { (/) } }