Theorem 2pwne

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

	Ref	Expression
Assertion	2pwne	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝒫 𝐴 ≠ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		sdomirr	⊢ ¬ 𝒫 𝒫 𝐴 ≺ 𝒫 𝒫 𝐴
2		canth2g	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≺ 𝒫 𝐴 )
3		pwexg	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
4		canth2g	⊢ ( 𝒫 𝐴 ∈ V → 𝒫 𝐴 ≺ 𝒫 𝒫 𝐴 )
5	3 4	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ≺ 𝒫 𝒫 𝐴 )
6		sdomtr	⊢ ( ( 𝐴 ≺ 𝒫 𝐴 ∧ 𝒫 𝐴 ≺ 𝒫 𝒫 𝐴 ) → 𝐴 ≺ 𝒫 𝒫 𝐴 )
7	2 5 6	syl2anc	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≺ 𝒫 𝒫 𝐴 )
8		breq1	⊢ ( 𝒫 𝒫 𝐴 = 𝐴 → ( 𝒫 𝒫 𝐴 ≺ 𝒫 𝒫 𝐴 ↔ 𝐴 ≺ 𝒫 𝒫 𝐴 ) )
9	7 8	syl5ibrcom	⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝒫 𝐴 = 𝐴 → 𝒫 𝒫 𝐴 ≺ 𝒫 𝒫 𝐴 ) )
10	1 9	mtoi	⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝒫 𝒫 𝐴 = 𝐴 )
11	10	neqned	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝒫 𝐴 ≠ 𝐴 )