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 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ^m ( B |_| C ) ) ~~ ( ( A ^m B ) X. ( A ^m C ) ) )

Proof

Step Hyp Ref Expression
1 df-dju 
 |-  ( B |_| C ) = ( ( { (/) } X. B ) u. ( { 1o } X. C ) )
2 1 oveq2i 
 |-  ( A ^m ( B |_| C ) ) = ( A ^m ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) )
3 snex 
 |-  { (/) } e. _V
4 simp2 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> B e. W )
5 xpexg 
 |-  ( ( { (/) } e. _V /\ B e. W ) -> ( { (/) } X. B ) e. _V )
6 3 4 5 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { (/) } X. B ) e. _V )
7 snex 
 |-  { 1o } e. _V
8 simp3 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> C e. X )
9 xpexg 
 |-  ( ( { 1o } e. _V /\ C e. X ) -> ( { 1o } X. C ) e. _V )
10 7 8 9 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { 1o } X. C ) e. _V )
11 simp1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> A e. V )
12 xp01disjl 
 |-  ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) = (/)
13 12 a1i 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) = (/) )
14 mapunen 
 |-  ( ( ( ( { (/) } X. B ) e. _V /\ ( { 1o } X. C ) e. _V /\ A e. V ) /\ ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) = (/) ) -> ( A ^m ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) ) ~~ ( ( A ^m ( { (/) } X. B ) ) X. ( A ^m ( { 1o } X. C ) ) ) )
15 6 10 11 13 14 syl31anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ^m ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) ) ~~ ( ( A ^m ( { (/) } X. B ) ) X. ( A ^m ( { 1o } X. C ) ) ) )
16 2 15 eqbrtrid 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ^m ( B |_| C ) ) ~~ ( ( A ^m ( { (/) } X. B ) ) X. ( A ^m ( { 1o } X. C ) ) ) )
17 enrefg 
 |-  ( A e. V -> A ~~ A )
18 11 17 syl 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> A ~~ A )
19 0ex 
 |-  (/) e. _V
20 xpsnen2g 
 |-  ( ( (/) e. _V /\ B e. W ) -> ( { (/) } X. B ) ~~ B )
21 19 4 20 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { (/) } X. B ) ~~ B )
22 mapen 
 |-  ( ( A ~~ A /\ ( { (/) } X. B ) ~~ B ) -> ( A ^m ( { (/) } X. B ) ) ~~ ( A ^m B ) )
23 18 21 22 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ^m ( { (/) } X. B ) ) ~~ ( A ^m B ) )
24 1on 
 |-  1o e. On
25 xpsnen2g 
 |-  ( ( 1o e. On /\ C e. X ) -> ( { 1o } X. C ) ~~ C )
26 24 8 25 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { 1o } X. C ) ~~ C )
27 mapen 
 |-  ( ( A ~~ A /\ ( { 1o } X. C ) ~~ C ) -> ( A ^m ( { 1o } X. C ) ) ~~ ( A ^m C ) )
28 18 26 27 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ^m ( { 1o } X. C ) ) ~~ ( A ^m C ) )
29 xpen 
 |-  ( ( ( A ^m ( { (/) } X. B ) ) ~~ ( A ^m B ) /\ ( A ^m ( { 1o } X. C ) ) ~~ ( A ^m C ) ) -> ( ( A ^m ( { (/) } X. B ) ) X. ( A ^m ( { 1o } X. C ) ) ) ~~ ( ( A ^m B ) X. ( A ^m C ) ) )
30 23 28 29 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ^m ( { (/) } X. B ) ) X. ( A ^m ( { 1o } X. C ) ) ) ~~ ( ( A ^m B ) X. ( A ^m C ) ) )
31 entr 
 |-  ( ( ( A ^m ( B |_| C ) ) ~~ ( ( A ^m ( { (/) } X. B ) ) X. ( A ^m ( { 1o } X. C ) ) ) /\ ( ( A ^m ( { (/) } X. B ) ) X. ( A ^m ( { 1o } X. C ) ) ) ~~ ( ( A ^m B ) X. ( A ^m C ) ) ) -> ( A ^m ( B |_| C ) ) ~~ ( ( A ^m B ) X. ( A ^m C ) ) )
32 16 30 31 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ^m ( B |_| C ) ) ~~ ( ( A ^m B ) X. ( A ^m C ) ) )