Theorem 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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 ( 𝐴 ⊔ 1o ) )

Proof

Step	Hyp	Ref	Expression
1		1on	⊢ 1o ∈ On
2		pwdjuen	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1o ∈ On ) → 𝒫 ( 𝐴 ⊔ 1o ) ≈ ( 𝒫 𝐴 × 𝒫 1o ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 ( 𝐴 ⊔ 1o ) ≈ ( 𝒫 𝐴 × 𝒫 1o ) )
4		pwexg	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
5		1oex	⊢ 1o ∈ V
6	5	pwex	⊢ 𝒫 1o ∈ V
7		xpcomeng	⊢ ( ( 𝒫 𝐴 ∈ V ∧ 𝒫 1o ∈ V ) → ( 𝒫 𝐴 × 𝒫 1o ) ≈ ( 𝒫 1o × 𝒫 𝐴 ) )
8	4 6 7	sylancl	⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 × 𝒫 1o ) ≈ ( 𝒫 1o × 𝒫 𝐴 ) )
9		entr	⊢ ( ( 𝒫 ( 𝐴 ⊔ 1o ) ≈ ( 𝒫 𝐴 × 𝒫 1o ) ∧ ( 𝒫 𝐴 × 𝒫 1o ) ≈ ( 𝒫 1o × 𝒫 𝐴 ) ) → 𝒫 ( 𝐴 ⊔ 1o ) ≈ ( 𝒫 1o × 𝒫 𝐴 ) )
10	3 8 9	syl2anc	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 ( 𝐴 ⊔ 1o ) ≈ ( 𝒫 1o × 𝒫 𝐴 ) )
11		pwpw0	⊢ 𝒫 { ∅ } = { ∅ , { ∅ } }
12		df1o2	⊢ 1o = { ∅ }
13	12	pweqi	⊢ 𝒫 1o = 𝒫 { ∅ }
14		df2o2	⊢ 2o = { ∅ , { ∅ } }
15	11 13 14	3eqtr4i	⊢ 𝒫 1o = 2o
16	15	xpeq1i	⊢ ( 𝒫 1o × 𝒫 𝐴 ) = ( 2o × 𝒫 𝐴 )
17		xp2dju	⊢ ( 2o × 𝒫 𝐴 ) = ( 𝒫 𝐴 ⊔ 𝒫 𝐴 )
18	16 17	eqtri	⊢ ( 𝒫 1o × 𝒫 𝐴 ) = ( 𝒫 𝐴 ⊔ 𝒫 𝐴 )
19	10 18	breqtrdi	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 ( 𝐴 ⊔ 1o ) ≈ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
20	19	ensymd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 ( 𝐴 ⊔ 1o ) )