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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝒫 𝐴 × 𝒫 𝐵 ) )