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

Metamath Proof Explorer

Theorem 2pwuninel

Description: The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by NM, 27-Jun-2008)

Ref Expression
Assertion 2pwuninel 
|- -. ~P ~P U. A e. A

Proof

Step Hyp Ref Expression
1 sdomirr 
 |-  -. ~P ~P U. A ~< ~P ~P U. A
2 elssuni 
 |-  ( ~P ~P U. A e. A -> ~P ~P U. A C_ U. A )
3 ssdomg 
 |-  ( U. A e. _V -> ( ~P ~P U. A C_ U. A -> ~P ~P U. A ~<_ U. A ) )
4 canth2g 
 |-  ( U. A e. _V -> U. A ~< ~P U. A )
5 pwexb 
 |-  ( U. A e. _V <-> ~P U. A e. _V )
6 canth2g 
 |-  ( ~P U. A e. _V -> ~P U. A ~< ~P ~P U. A )
7 5 6 sylbi 
 |-  ( U. A e. _V -> ~P U. A ~< ~P ~P U. A )
8 sdomtr 
 |-  ( ( U. A ~< ~P U. A /\ ~P U. A ~< ~P ~P U. A ) -> U. A ~< ~P ~P U. A )
9 4 7 8 syl2anc 
 |-  ( U. A e. _V -> U. A ~< ~P ~P U. A )
10 domsdomtr 
 |-  ( ( ~P ~P U. A ~<_ U. A /\ U. A ~< ~P ~P U. A ) -> ~P ~P U. A ~< ~P ~P U. A )
11 10 ex 
 |-  ( ~P ~P U. A ~<_ U. A -> ( U. A ~< ~P ~P U. A -> ~P ~P U. A ~< ~P ~P U. A ) )
12 3 9 11 syl6ci 
 |-  ( U. A e. _V -> ( ~P ~P U. A C_ U. A -> ~P ~P U. A ~< ~P ~P U. A ) )
13 2 12 syl5 
 |-  ( U. A e. _V -> ( ~P ~P U. A e. A -> ~P ~P U. A ~< ~P ~P U. A ) )
14 1 13 mtoi 
 |-  ( U. A e. _V -> -. ~P ~P U. A e. A )
15 elex 
 |-  ( ~P ~P U. A e. A -> ~P ~P U. A e. _V )
16 pwexb 
 |-  ( ~P U. A e. _V <-> ~P ~P U. A e. _V )
17 5 16 bitri 
 |-  ( U. A e. _V <-> ~P ~P U. A e. _V )
18 15 17 sylibr 
 |-  ( ~P ~P U. A e. A -> U. A e. _V )
19 18 con3i 
 |-  ( -. U. A e. _V -> -. ~P ~P U. A e. A )
20 14 19 pm2.61i 
 |-  -. ~P ~P U. A e. A