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	$$⊢\neg 𝒫𝒫\bigcup A\in A$$

Proof

Step	Hyp	Ref	Expression
1		sdomirr	$$⊢\neg 𝒫𝒫\bigcup A\prec 𝒫𝒫\bigcup A$$
2		elssuni	$$⊢𝒫𝒫\bigcup A\in A\to 𝒫𝒫\bigcup A\subseteq \bigcup A$$
3		ssdomg	$$⊢\bigcup A\in \mathrm{V}\to \left(𝒫𝒫\bigcup A\subseteq \bigcup A\to 𝒫𝒫\bigcup A\preccurlyeq \bigcup A\right)$$
4		canth2g	$$⊢\bigcup A\in \mathrm{V}\to \bigcup A\prec 𝒫\bigcup A$$
5		pwexb	$$⊢\bigcup A\in \mathrm{V}\leftrightarrow 𝒫\bigcup A\in \mathrm{V}$$
6		canth2g	$$⊢𝒫\bigcup A\in \mathrm{V}\to 𝒫\bigcup A\prec 𝒫𝒫\bigcup A$$
7	5 6	sylbi	$$⊢\bigcup A\in \mathrm{V}\to 𝒫\bigcup A\prec 𝒫𝒫\bigcup A$$
8		sdomtr	$$⊢\left(\bigcup A\prec 𝒫\bigcup A\wedge 𝒫\bigcup A\prec 𝒫𝒫\bigcup A\right)\to \bigcup A\prec 𝒫𝒫\bigcup A$$
9	4 7 8	syl2anc	$$⊢\bigcup A\in \mathrm{V}\to \bigcup A\prec 𝒫𝒫\bigcup A$$
10		domsdomtr	$$⊢\left(𝒫𝒫\bigcup A\preccurlyeq \bigcup A\wedge \bigcup A\prec 𝒫𝒫\bigcup A\right)\to 𝒫𝒫\bigcup A\prec 𝒫𝒫\bigcup A$$
11	10	ex	$$⊢𝒫𝒫\bigcup A\preccurlyeq \bigcup A\to \left(\bigcup A\prec 𝒫𝒫\bigcup A\to 𝒫𝒫\bigcup A\prec 𝒫𝒫\bigcup A\right)$$
12	3 9 11	syl6ci	$$⊢\bigcup A\in \mathrm{V}\to \left(𝒫𝒫\bigcup A\subseteq \bigcup A\to 𝒫𝒫\bigcup A\prec 𝒫𝒫\bigcup A\right)$$
13	2 12	syl5	$$⊢\bigcup A\in \mathrm{V}\to \left(𝒫𝒫\bigcup A\in A\to 𝒫𝒫\bigcup A\prec 𝒫𝒫\bigcup A\right)$$
14	1 13	mtoi	$$⊢\bigcup A\in \mathrm{V}\to \neg 𝒫𝒫\bigcup A\in A$$
15		elex	$$⊢𝒫𝒫\bigcup A\in A\to 𝒫𝒫\bigcup A\in \mathrm{V}$$
16		pwexb	$$⊢𝒫\bigcup A\in \mathrm{V}\leftrightarrow 𝒫𝒫\bigcup A\in \mathrm{V}$$
17	5 16	bitri	$$⊢\bigcup A\in \mathrm{V}\leftrightarrow 𝒫𝒫\bigcup A\in \mathrm{V}$$
18	15 17	sylibr	$$⊢𝒫𝒫\bigcup A\in A\to \bigcup A\in \mathrm{V}$$
19	18	con3i	$$⊢\neg \bigcup A\in \mathrm{V}\to \neg 𝒫𝒫\bigcup A\in A$$
20	14 19	pm2.61i	$$⊢\neg 𝒫𝒫\bigcup A\in A$$