Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mappwen Structured version   Unicode version

Theorem mappwen 8525
 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.)
Assertion
Ref Expression
mappwen

Proof of Theorem mappwen
StepHypRef Expression
1 simprr 758 . . . . 5
2 pw2eng 7661 . . . . . 6
32ad2antrr 724 . . . . 5
4 domentr 7612 . . . . 5
51, 3, 4syl2anc 659 . . . 4
6 mapdom1 7720 . . . 4
75, 6syl 17 . . 3
8 2on 7175 . . . . . . 7
98a1i 11 . . . . . 6
10 simpll 752 . . . . . 6
11 mapxpen 7721 . . . . . 6
129, 10, 10, 11syl3anc 1230 . . . . 5
138elexi 3069 . . . . . . 7
1413enref 7586 . . . . . 6
15 infxpidm2 8426 . . . . . . 7
1615adantr 463 . . . . . 6
17 mapen 7719 . . . . . 6
1814, 16, 17sylancr 661 . . . . 5
19 entr 7605 . . . . 5
2012, 18, 19syl2anc 659 . . . 4
213ensymd 7604 . . . 4
22 entr 7605 . . . 4
2320, 21, 22syl2anc 659 . . 3
24 domentr 7612 . . 3
257, 23, 24syl2anc 659 . 2
26 mapdom1 7720 . . . 4