Metamath Proof Explorer

Theorem pwdjuen

Description: Sum of exponents law for cardinal arithmetic. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	pwdjuen	$⊢ (A \in V \land B \in W) \to 𝒫 (A ⊔︀ B) \approx (𝒫 A \times 𝒫 B)$

Proof

Step	Hyp	Ref	Expression
1		djuex	$⊢ (A \in V \land B \in W) \to (A ⊔︀ B) \in V$
2		pw2eng	$⊢ (A ⊔︀ B) \in V \to 𝒫 (A ⊔︀ B) \approx ({2_{𝑜}}^{(A ⊔︀ B)})$
3	1 2	syl	$⊢ (A \in V \land B \in W) \to 𝒫 (A ⊔︀ B) \approx ({2_{𝑜}}^{(A ⊔︀ B)})$
4		2on	$⊢ 2_{𝑜} \in On$
5		mapdjuen	$⊢ (2_{𝑜} \in On \land A \in V \land B \in W) \to ({2_{𝑜}}^{(A ⊔︀ B)}) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{B}))$
6	4 5	mp3an1	$⊢ (A \in V \land B \in W) \to ({2_{𝑜}}^{(A ⊔︀ B)}) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{B}))$
7		pw2eng	$⊢ A \in V \to 𝒫 A \approx ({2_{𝑜}}^{A})$
8		pw2eng	$⊢ B \in W \to 𝒫 B \approx ({2_{𝑜}}^{B})$
9		xpen	$⊢ (𝒫 A \approx ({2_{𝑜}}^{A}) \land 𝒫 B \approx ({2_{𝑜}}^{B})) \to (𝒫 A \times 𝒫 B) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{B}))$
10	7 8 9	syl2an	$⊢ (A \in V \land B \in W) \to (𝒫 A \times 𝒫 B) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{B}))$
11		enen2	$⊢ (𝒫 A \times 𝒫 B) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{B})) \to (({2_{𝑜}}^{(A ⊔︀ B)}) \approx (𝒫 A \times 𝒫 B) \leftrightarrow ({2_{𝑜}}^{(A ⊔︀ B)}) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{B})))$
12	10 11	syl	$⊢ (A \in V \land B \in W) \to (({2_{𝑜}}^{(A ⊔︀ B)}) \approx (𝒫 A \times 𝒫 B) \leftrightarrow ({2_{𝑜}}^{(A ⊔︀ B)}) \approx (({2_{𝑜}}^{A}) \times ({2_{𝑜}}^{B})))$
13	6 12	mpbird	$⊢ (A \in V \land B \in W) \to ({2_{𝑜}}^{(A ⊔︀ B)}) \approx (𝒫 A \times 𝒫 B)$
14		entr	$⊢ (𝒫 (A ⊔︀ B) \approx ({2_{𝑜}}^{(A ⊔︀ B)}) \land ({2_{𝑜}}^{(A ⊔︀ B)}) \approx (𝒫 A \times 𝒫 B)) \to 𝒫 (A ⊔︀ B) \approx (𝒫 A \times 𝒫 B)$
15	3 13 14	syl2anc	$⊢ (A \in V \land B \in W) \to 𝒫 (A ⊔︀ B) \approx (𝒫 A \times 𝒫 B)$