This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )