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

Metamath Proof Explorer

Theorem pwdjuen

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

Ref Expression
Assertion pwdjuen ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝒫 𝐴 × 𝒫 𝐵 ) )

Proof

Step Hyp Ref Expression
1 djuex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ∈ V )
2 pw2eng ⊢ ( ( 𝐴 ⊔ 𝐵 ) ∈ V → 𝒫 ( 𝐴 ⊔ 𝐵 ) ≈ ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) )
3 1 2 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 ⊔ 𝐵 ) ≈ ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) )
4 2on ⊢ 2o ∈ On
5 mapdjuen ⊢ ( ( 2o ∈ On ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m 𝐵 ) ) )
6 4 5 mp3an1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m 𝐵 ) ) )
7 pw2eng ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )
8 pw2eng ⊢ ( 𝐵 ∈ 𝑊 → 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) )
9 xpen ⊢ ( ( 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) ∧ 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) ) → ( 𝒫 𝐴 × 𝒫 𝐵 ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m 𝐵 ) ) )
10 7 8 9 syl2an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝒫 𝐴 × 𝒫 𝐵 ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m 𝐵 ) ) )
11 enen2 ⊢ ( ( 𝒫 𝐴 × 𝒫 𝐵 ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m 𝐵 ) ) → ( ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) ≈ ( 𝒫 𝐴 × 𝒫 𝐵 ) ↔ ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m 𝐵 ) ) ) )
12 10 11 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) ≈ ( 𝒫 𝐴 × 𝒫 𝐵 ) ↔ ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) ≈ ( ( 2o ↑m 𝐴 ) × ( 2o ↑m 𝐵 ) ) ) )
13 6 12 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) ≈ ( 𝒫 𝐴 × 𝒫 𝐵 ) )
14 entr ⊢ ( ( 𝒫 ( 𝐴 ⊔ 𝐵 ) ≈ ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) ∧ ( 2o ↑m ( 𝐴 ⊔ 𝐵 ) ) ≈ ( 𝒫 𝐴 × 𝒫 𝐵 ) ) → 𝒫 ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝒫 𝐴 × 𝒫 𝐵 ) )
15 3 13 14 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝒫 𝐴 × 𝒫 𝐵 ) )