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

Theorem mappwen 7623
 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 736 . . . . 5
2 pw2eng 6853 . . . . . 6
32ad2antrr 709 . . . . 5
4 domentr 6805 . . . . 5
51, 3, 4syl2anc 645 . . . 4
6 mapdom1 6911 . . . 4
75, 6syl 17 . . 3
8 2on 6373 . . . . . . 7
98a1i 12 . . . . . 6
10 simpll 733 . . . . . 6
11 mapxpen 6912 . . . . . 6
129, 10, 10, 11syl3anc 1187 . . . . 5
138elexi 2736 . . . . . . 7
1413enref 6780 . . . . . 6
15 infxpidm2 7528 . . . . . . 7
1615adantr 453 . . . . . 6
17 mapen 6910 . . . . . 6
1814, 16, 17sylancr 647 . . . . 5
19 entr 6798 . . . . 5
2012, 18, 19syl2anc 645 . . . 4
21 ensym 6796 . . . . 5
223, 21syl 17 . . . 4
23 entr 6798 . . . 4
2420, 22, 23syl2anc 645 . . 3
25 domentr 6805 . . 3
267, 24, 25syl2anc 645 . 2
27 mapdom1 6911 . . . 4