Theorem 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	⊢ ( ω ≼ 𝐴 → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		reldom	⊢ Rel ≼
2	1	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
3		pwdju1	⊢ ( 𝐴 ∈ V → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 ( 𝐴 ⊔ 1o ) )
4	2 3	syl	⊢ ( ω ≼ 𝐴 → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 ( 𝐴 ⊔ 1o ) )
5		infdju1	⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )
6		pwen	⊢ ( ( 𝐴 ⊔ 1o ) ≈ 𝐴 → 𝒫 ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 )
7	5 6	syl	⊢ ( ω ≼ 𝐴 → 𝒫 ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 )
8		entr	⊢ ( ( ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 ( 𝐴 ⊔ 1o ) ∧ 𝒫 ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 ) → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 𝐴 )
9	4 7 8	syl2anc	⊢ ( ω ≼ 𝐴 → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 𝐴 )