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