# 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 ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({{A}}^{{B}}\right)\approx 𝒫{B}$

### Proof

Step Hyp Ref Expression
1 simprr ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to {A}\preccurlyeq 𝒫{B}$
2 pw2eng ${⊢}{B}\in \mathrm{dom}\mathrm{card}\to 𝒫{B}\approx \left({{2}_{𝑜}}^{{B}}\right)$
3 2 ad2antrr ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to 𝒫{B}\approx \left({{2}_{𝑜}}^{{B}}\right)$
4 domentr ${⊢}\left({A}\preccurlyeq 𝒫{B}\wedge 𝒫{B}\approx \left({{2}_{𝑜}}^{{B}}\right)\right)\to {A}\preccurlyeq \left({{2}_{𝑜}}^{{B}}\right)$
5 1 3 4 syl2anc ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to {A}\preccurlyeq \left({{2}_{𝑜}}^{{B}}\right)$
6 mapdom1 ${⊢}{A}\preccurlyeq \left({{2}_{𝑜}}^{{B}}\right)\to \left({{A}}^{{B}}\right)\preccurlyeq \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)$
7 5 6 syl ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({{A}}^{{B}}\right)\preccurlyeq \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)$
8 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
9 simpll ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to {B}\in \mathrm{dom}\mathrm{card}$
10 mapxpen ${⊢}\left({2}_{𝑜}\in \mathrm{On}\wedge {B}\in \mathrm{dom}\mathrm{card}\wedge {B}\in \mathrm{dom}\mathrm{card}\right)\to \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\approx \left({{2}_{𝑜}}^{\left({B}×{B}\right)}\right)$
11 8 9 9 10 mp3an2i ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\approx \left({{2}_{𝑜}}^{\left({B}×{B}\right)}\right)$
12 8 elexi ${⊢}{2}_{𝑜}\in \mathrm{V}$
13 12 enref ${⊢}{2}_{𝑜}\approx {2}_{𝑜}$
14 infxpidm2 ${⊢}\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\to \left({B}×{B}\right)\approx {B}$
15 14 adantr ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({B}×{B}\right)\approx {B}$
16 mapen ${⊢}\left({2}_{𝑜}\approx {2}_{𝑜}\wedge \left({B}×{B}\right)\approx {B}\right)\to \left({{2}_{𝑜}}^{\left({B}×{B}\right)}\right)\approx \left({{2}_{𝑜}}^{{B}}\right)$
17 13 15 16 sylancr ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({{2}_{𝑜}}^{\left({B}×{B}\right)}\right)\approx \left({{2}_{𝑜}}^{{B}}\right)$
18 entr ${⊢}\left(\left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\approx \left({{2}_{𝑜}}^{\left({B}×{B}\right)}\right)\wedge \left({{2}_{𝑜}}^{\left({B}×{B}\right)}\right)\approx \left({{2}_{𝑜}}^{{B}}\right)\right)\to \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\approx \left({{2}_{𝑜}}^{{B}}\right)$
19 11 17 18 syl2anc ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\approx \left({{2}_{𝑜}}^{{B}}\right)$
20 3 ensymd ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({{2}_{𝑜}}^{{B}}\right)\approx 𝒫{B}$
21 entr ${⊢}\left(\left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\approx \left({{2}_{𝑜}}^{{B}}\right)\wedge \left({{2}_{𝑜}}^{{B}}\right)\approx 𝒫{B}\right)\to \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\approx 𝒫{B}$
22 19 20 21 syl2anc ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\approx 𝒫{B}$
23 domentr ${⊢}\left(\left({{A}}^{{B}}\right)\preccurlyeq \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\wedge \left({\left({{2}_{𝑜}}^{{B}}\right)}^{{B}}\right)\approx 𝒫{B}\right)\to \left({{A}}^{{B}}\right)\preccurlyeq 𝒫{B}$
24 7 22 23 syl2anc ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({{A}}^{{B}}\right)\preccurlyeq 𝒫{B}$
25 mapdom1 ${⊢}{2}_{𝑜}\preccurlyeq {A}\to \left({{2}_{𝑜}}^{{B}}\right)\preccurlyeq \left({{A}}^{{B}}\right)$
26 25 ad2antrl ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({{2}_{𝑜}}^{{B}}\right)\preccurlyeq \left({{A}}^{{B}}\right)$
27 endomtr ${⊢}\left(𝒫{B}\approx \left({{2}_{𝑜}}^{{B}}\right)\wedge \left({{2}_{𝑜}}^{{B}}\right)\preccurlyeq \left({{A}}^{{B}}\right)\right)\to 𝒫{B}\preccurlyeq \left({{A}}^{{B}}\right)$
28 3 26 27 syl2anc ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to 𝒫{B}\preccurlyeq \left({{A}}^{{B}}\right)$
29 sbth ${⊢}\left(\left({{A}}^{{B}}\right)\preccurlyeq 𝒫{B}\wedge 𝒫{B}\preccurlyeq \left({{A}}^{{B}}\right)\right)\to \left({{A}}^{{B}}\right)\approx 𝒫{B}$
30 24 28 29 syl2anc ${⊢}\left(\left({B}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {B}\right)\wedge \left({2}_{𝑜}\preccurlyeq {A}\wedge {A}\preccurlyeq 𝒫{B}\right)\right)\to \left({{A}}^{{B}}\right)\approx 𝒫{B}$