pwdju1

Description: The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	pwdju1	$⊢ A \in V \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 (A ⊔︀ 1_{𝑜})$

Step	Hyp	Ref	Expression
1		1on	$⊢ 1_{𝑜} \in On$
2		pwdjuen	$⊢ (A \in V \land 1_{𝑜} \in On) \to 𝒫 (A ⊔︀ 1_{𝑜}) \approx (𝒫 A \times 𝒫 1_{𝑜})$
3	1 2	mpan2	$⊢ A \in V \to 𝒫 (A ⊔︀ 1_{𝑜}) \approx (𝒫 A \times 𝒫 1_{𝑜})$
4		pwexg	$⊢ A \in V \to 𝒫 A \in V$
5		1oex	$⊢ 1_{𝑜} \in V$
6	5	pwex	$⊢ 𝒫 1_{𝑜} \in V$
7		xpcomeng	$⊢ (𝒫 A \in V \land 𝒫 1_{𝑜} \in V) \to (𝒫 A \times 𝒫 1_{𝑜}) \approx (𝒫 1_{𝑜} \times 𝒫 A)$
8	4 6 7	sylancl	$⊢ A \in V \to (𝒫 A \times 𝒫 1_{𝑜}) \approx (𝒫 1_{𝑜} \times 𝒫 A)$
9		entr	$⊢ (𝒫 (A ⊔︀ 1_{𝑜}) \approx (𝒫 A \times 𝒫 1_{𝑜}) \land (𝒫 A \times 𝒫 1_{𝑜}) \approx (𝒫 1_{𝑜} \times 𝒫 A)) \to 𝒫 (A ⊔︀ 1_{𝑜}) \approx (𝒫 1_{𝑜} \times 𝒫 A)$
10	3 8 9	syl2anc	$⊢ A \in V \to 𝒫 (A ⊔︀ 1_{𝑜}) \approx (𝒫 1_{𝑜} \times 𝒫 A)$
11		pwpw0	$⊢ 𝒫 \{\emptyset\} = \{\emptyset, \{\emptyset\}\}$
12		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
13	12	pweqi	$⊢ 𝒫 1_{𝑜} = 𝒫 \{\emptyset\}$
14		df2o2	$⊢ 2_{𝑜} = \{\emptyset, \{\emptyset\}\}$
15	11 13 14	3eqtr4i	$⊢ 𝒫 1_{𝑜} = 2_{𝑜}$
16	15	xpeq1i	$⊢ 𝒫 1_{𝑜} \times 𝒫 A = 2_{𝑜} \times 𝒫 A$
17		xp2dju	$⊢ 2_{𝑜} \times 𝒫 A = (𝒫 A ⊔︀ 𝒫 A)$
18	16 17	eqtri	$⊢ 𝒫 1_{𝑜} \times 𝒫 A = (𝒫 A ⊔︀ 𝒫 A)$
19	10 18	breqtrdi	$⊢ A \in V \to 𝒫 (A ⊔︀ 1_{𝑜}) \approx (𝒫 A ⊔︀ 𝒫 A)$
20	19	ensymd	$⊢ A \in V \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 (A ⊔︀ 1_{𝑜})$

Metamath Proof Explorer