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

Metamath Proof Explorer

Theorem mapdjuen

Description: Sum of exponents law for cardinal arithmetic. Theorem 6I(4) of Enderton p. 142. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion mapdjuen ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 df-dju ⊢ ( 𝐵 ⊔ 𝐶 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) )
2 1 oveq2i ⊢ ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) = ( 𝐴 ↑m ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) )
3 snex ⊢ { ∅ } ∈ V
4 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ 𝑊 )
5 xpexg ⊢ ( ( { ∅ } ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ∈ V )
6 3 4 5 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐵 ) ∈ V )
7 snex ⊢ { 1o } ∈ V
8 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 )
9 xpexg ⊢ ( ( { 1o } ∈ V ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ∈ V )
10 7 8 9 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ∈ V )
11 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ∈ 𝑉 )
12 xp01disjl ⊢ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅
13 12 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅ )
14 mapunen ⊢ ( ( ( ( { ∅ } × 𝐵 ) ∈ V ∧ ( { 1o } × 𝐶 ) ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅ ) → ( 𝐴 ↑m ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) )
15 6 10 11 13 14 syl31anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) )
16 2 15 eqbrtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) )
17 enrefg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴 )
18 11 17 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ≈ 𝐴 )
19 0ex ⊢ ∅ ∈ V
20 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
21 19 4 20 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
22 mapen ⊢ ( ( 𝐴 ≈ 𝐴 ∧ ( { ∅ } × 𝐵 ) ≈ 𝐵 ) → ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) ≈ ( 𝐴 ↑m 𝐵 ) )
23 18 21 22 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) ≈ ( 𝐴 ↑m 𝐵 ) )
24 1on ⊢ 1o ∈ On
25 xpsnen2g ⊢ ( ( 1o ∈ On ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 )
26 24 8 25 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 )
27 mapen ⊢ ( ( 𝐴 ≈ 𝐴 ∧ ( { 1o } × 𝐶 ) ≈ 𝐶 ) → ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ≈ ( 𝐴 ↑m 𝐶 ) )
28 18 26 27 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ≈ ( 𝐴 ↑m 𝐶 ) )
29 xpen ⊢ ( ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) ≈ ( 𝐴 ↑m 𝐵 ) ∧ ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ≈ ( 𝐴 ↑m 𝐶 ) ) → ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) )
30 23 28 29 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) )
31 entr ⊢ ( ( ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ∧ ( ( 𝐴 ↑m ( { ∅ } × 𝐵 ) ) × ( 𝐴 ↑m ( { 1o } × 𝐶 ) ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) ) → ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) )
32 16 30 31 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ↑m ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 ↑m 𝐵 ) × ( 𝐴 ↑m 𝐶 ) ) )