pwdjuidm

Description: If the natural numbers inject into A , then ~P A is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	pwdjuidm	$⊢ ω ≼ A \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 A$

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2	1	brrelex2i	$⊢ ω ≼ A \to A \in V$
3		pwdju1	$⊢ A \in V \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 (A ⊔︀ 1_{𝑜})$
4	2 3	syl	$⊢ ω ≼ A \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 (A ⊔︀ 1_{𝑜})$
5		infdju1	$⊢ ω ≼ A \to (A ⊔︀ 1_{𝑜}) \approx A$
6		pwen	$⊢ (A ⊔︀ 1_{𝑜}) \approx A \to 𝒫 (A ⊔︀ 1_{𝑜}) \approx 𝒫 A$
7	5 6	syl	$⊢ ω ≼ A \to 𝒫 (A ⊔︀ 1_{𝑜}) \approx 𝒫 A$
8		entr	$⊢ ((𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 (A ⊔︀ 1_{𝑜}) \land 𝒫 (A ⊔︀ 1_{𝑜}) \approx 𝒫 A) \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 A$
9	4 7 8	syl2anc	$⊢ ω ≼ A \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 A$

Metamath Proof Explorer