Metamath Proof Explorer

Theorem 2pwne

Description: No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008)

Ref Expression
Assertion 2pwne 
|- ( A e. V -> ~P ~P A =/= A )

Proof

Step Hyp Ref Expression
1 sdomirr 
 |-  -. ~P ~P A ~< ~P ~P A
2 canth2g 
 |-  ( A e. V -> A ~< ~P A )
3 pwexg 
 |-  ( A e. V -> ~P A e. _V )
4 canth2g 
 |-  ( ~P A e. _V -> ~P A ~< ~P ~P A )
5 3 4 syl 
 |-  ( A e. V -> ~P A ~< ~P ~P A )
6 sdomtr 
 |-  ( ( A ~< ~P A /\ ~P A ~< ~P ~P A ) -> A ~< ~P ~P A )
7 2 5 6 syl2anc 
 |-  ( A e. V -> A ~< ~P ~P A )
8 breq1 
 |-  ( ~P ~P A = A -> ( ~P ~P A ~< ~P ~P A <-> A ~< ~P ~P A ) )
9 7 8 syl5ibrcom 
 |-  ( A e. V -> ( ~P ~P A = A -> ~P ~P A ~< ~P ~P A ) )
10 1 9 mtoi 
 |-  ( A e. V -> -. ~P ~P A = A )
11 10 neqned 
 |-  ( A e. V -> ~P ~P A =/= A )