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	⊢ ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		sdomirr	⊢ ¬ 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴
2		elssuni	⊢ ( 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ⊆ ∪ 𝐴 )
3		ssdomg	⊢ ( ∪ 𝐴 ∈ V → ( 𝒫 𝒫 ∪ 𝐴 ⊆ ∪ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ≼ ∪ 𝐴 ) )
4		canth2g	⊢ ( ∪ 𝐴 ∈ V → ∪ 𝐴 ≺ 𝒫 ∪ 𝐴 )
5		pwexb	⊢ ( ∪ 𝐴 ∈ V ↔ 𝒫 ∪ 𝐴 ∈ V )
6		canth2g	⊢ ( 𝒫 ∪ 𝐴 ∈ V → 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
7	5 6	sylbi	⊢ ( ∪ 𝐴 ∈ V → 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
8		sdomtr	⊢ ( ( ∪ 𝐴 ≺ 𝒫 ∪ 𝐴 ∧ 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) → ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
9	4 7 8	syl2anc	⊢ ( ∪ 𝐴 ∈ V → ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
10		domsdomtr	⊢ ( ( 𝒫 𝒫 ∪ 𝐴 ≼ ∪ 𝐴 ∧ ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) → 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
11	10	ex	⊢ ( 𝒫 𝒫 ∪ 𝐴 ≼ ∪ 𝐴 → ( ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) )
12	3 9 11	syl6ci	⊢ ( ∪ 𝐴 ∈ V → ( 𝒫 𝒫 ∪ 𝐴 ⊆ ∪ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) )
13	2 12	syl5	⊢ ( ∪ 𝐴 ∈ V → ( 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) )
14	1 13	mtoi	⊢ ( ∪ 𝐴 ∈ V → ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 )
15		elex	⊢ ( 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ∈ V )
16		pwexb	⊢ ( 𝒫 ∪ 𝐴 ∈ V ↔ 𝒫 𝒫 ∪ 𝐴 ∈ V )
17	5 16	bitri	⊢ ( ∪ 𝐴 ∈ V ↔ 𝒫 𝒫 ∪ 𝐴 ∈ V )
18	15 17	sylibr	⊢ ( 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 ∈ V )
19	18	con3i	⊢ ( ¬ ∪ 𝐴 ∈ V → ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 )
20	14 19	pm2.61i	⊢ ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴