2pwne

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

		Ref	Expression
	Assertion	2pwne	$⊢ A \in V \to 𝒫 𝒫 A \neq A$

Step	Hyp	Ref	Expression
1		sdomirr	$⊢ \neg 𝒫 𝒫 A ≺ 𝒫 𝒫 A$
2		canth2g	$⊢ A \in V \to A ≺ 𝒫 A$
3		pwexg	$⊢ A \in V \to 𝒫 A \in V$
4		canth2g	$⊢ 𝒫 A \in V \to 𝒫 A ≺ 𝒫 𝒫 A$
5	3 4	syl	$⊢ A \in V \to 𝒫 A ≺ 𝒫 𝒫 A$
6		sdomtr	$⊢ (A ≺ 𝒫 A \land 𝒫 A ≺ 𝒫 𝒫 A) \to A ≺ 𝒫 𝒫 A$
7	2 5 6	syl2anc	$⊢ A \in V \to A ≺ 𝒫 𝒫 A$
8		breq1	$⊢ 𝒫 𝒫 A = A \to (𝒫 𝒫 A ≺ 𝒫 𝒫 A \leftrightarrow A ≺ 𝒫 𝒫 A)$
9	7 8	syl5ibrcom	$⊢ A \in V \to (𝒫 𝒫 A = A \to 𝒫 𝒫 A ≺ 𝒫 𝒫 A)$
10	1 9	mtoi	$⊢ A \in V \to \neg 𝒫 𝒫 A = A$
11	10	neqned	$⊢ A \in V \to 𝒫 𝒫 A \neq A$

Metamath Proof Explorer