Metamath Proof Explorer

Theorem mappwen

Description: Power rule for cardinal arithmetic. Theorem 11.21 of TakeutiZaring p. 106. (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion mappwen 
|- ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( A ^m B ) ~~ ~P B )

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> A ~<_ ~P B )
2 pw2eng 
 |-  ( B e. dom card -> ~P B ~~ ( 2o ^m B ) )
3 2 ad2antrr 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ~P B ~~ ( 2o ^m B ) )
4 domentr 
 |-  ( ( A ~<_ ~P B /\ ~P B ~~ ( 2o ^m B ) ) -> A ~<_ ( 2o ^m B ) )
5 1 3 4 syl2anc 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> A ~<_ ( 2o ^m B ) )
6 mapdom1 
 |-  ( A ~<_ ( 2o ^m B ) -> ( A ^m B ) ~<_ ( ( 2o ^m B ) ^m B ) )
7 5 6 syl 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( A ^m B ) ~<_ ( ( 2o ^m B ) ^m B ) )
8 2on 
 |-  2o e. On
9 simpll 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> B e. dom card )
10 mapxpen 
 |-  ( ( 2o e. On /\ B e. dom card /\ B e. dom card ) -> ( ( 2o ^m B ) ^m B ) ~~ ( 2o ^m ( B X. B ) ) )
11 8 9 9 10 mp3an2i 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( ( 2o ^m B ) ^m B ) ~~ ( 2o ^m ( B X. B ) ) )
12 8 elexi 
 |-  2o e. _V
13 12 enref 
 |-  2o ~~ 2o
14 infxpidm2 
 |-  ( ( B e. dom card /\ _om ~<_ B ) -> ( B X. B ) ~~ B )
15 14 adantr 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( B X. B ) ~~ B )
16 mapen 
 |-  ( ( 2o ~~ 2o /\ ( B X. B ) ~~ B ) -> ( 2o ^m ( B X. B ) ) ~~ ( 2o ^m B ) )
17 13 15 16 sylancr 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( 2o ^m ( B X. B ) ) ~~ ( 2o ^m B ) )
18 entr 
 |-  ( ( ( ( 2o ^m B ) ^m B ) ~~ ( 2o ^m ( B X. B ) ) /\ ( 2o ^m ( B X. B ) ) ~~ ( 2o ^m B ) ) -> ( ( 2o ^m B ) ^m B ) ~~ ( 2o ^m B ) )
19 11 17 18 syl2anc 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( ( 2o ^m B ) ^m B ) ~~ ( 2o ^m B ) )
20 3 ensymd 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( 2o ^m B ) ~~ ~P B )
21 entr 
 |-  ( ( ( ( 2o ^m B ) ^m B ) ~~ ( 2o ^m B ) /\ ( 2o ^m B ) ~~ ~P B ) -> ( ( 2o ^m B ) ^m B ) ~~ ~P B )
22 19 20 21 syl2anc 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( ( 2o ^m B ) ^m B ) ~~ ~P B )
23 domentr 
 |-  ( ( ( A ^m B ) ~<_ ( ( 2o ^m B ) ^m B ) /\ ( ( 2o ^m B ) ^m B ) ~~ ~P B ) -> ( A ^m B ) ~<_ ~P B )
24 7 22 23 syl2anc 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( A ^m B ) ~<_ ~P B )
25 mapdom1 
 |-  ( 2o ~<_ A -> ( 2o ^m B ) ~<_ ( A ^m B ) )
26 25 ad2antrl 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( 2o ^m B ) ~<_ ( A ^m B ) )
27 endomtr 
 |-  ( ( ~P B ~~ ( 2o ^m B ) /\ ( 2o ^m B ) ~<_ ( A ^m B ) ) -> ~P B ~<_ ( A ^m B ) )
28 3 26 27 syl2anc 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ~P B ~<_ ( A ^m B ) )
29 sbth 
 |-  ( ( ( A ^m B ) ~<_ ~P B /\ ~P B ~<_ ( A ^m B ) ) -> ( A ^m B ) ~~ ~P B )
30 24 28 29 syl2anc 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( A ^m B ) ~~ ~P B )