# 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 ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐴m 𝐵 ) ≈ 𝒫 𝐵 )

### Proof

Step Hyp Ref Expression
1 simprr ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → 𝐴 ≼ 𝒫 𝐵 )
2 pw2eng ( 𝐵 ∈ dom card → 𝒫 𝐵 ≈ ( 2om 𝐵 ) )
3 2 ad2antrr ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → 𝒫 𝐵 ≈ ( 2om 𝐵 ) )
4 domentr ( ( 𝐴 ≼ 𝒫 𝐵 ∧ 𝒫 𝐵 ≈ ( 2om 𝐵 ) ) → 𝐴 ≼ ( 2om 𝐵 ) )
5 1 3 4 syl2anc ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → 𝐴 ≼ ( 2om 𝐵 ) )
6 mapdom1 ( 𝐴 ≼ ( 2om 𝐵 ) → ( 𝐴m 𝐵 ) ≼ ( ( 2om 𝐵 ) ↑m 𝐵 ) )
7 5 6 syl ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐴m 𝐵 ) ≼ ( ( 2om 𝐵 ) ↑m 𝐵 ) )
8 2on 2o ∈ On
9 simpll ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → 𝐵 ∈ dom card )
10 mapxpen ( ( 2o ∈ On ∧ 𝐵 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( 2om 𝐵 ) ↑m 𝐵 ) ≈ ( 2om ( 𝐵 × 𝐵 ) ) )
11 8 9 9 10 mp3an2i ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( ( 2om 𝐵 ) ↑m 𝐵 ) ≈ ( 2om ( 𝐵 × 𝐵 ) ) )
12 8 elexi 2o ∈ V
13 12 enref 2o ≈ 2o
14 infxpidm2 ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) → ( 𝐵 × 𝐵 ) ≈ 𝐵 )
15 14 adantr ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐵 × 𝐵 ) ≈ 𝐵 )
16 mapen ( ( 2o ≈ 2o ∧ ( 𝐵 × 𝐵 ) ≈ 𝐵 ) → ( 2om ( 𝐵 × 𝐵 ) ) ≈ ( 2om 𝐵 ) )
17 13 15 16 sylancr ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( 2om ( 𝐵 × 𝐵 ) ) ≈ ( 2om 𝐵 ) )
18 entr ( ( ( ( 2om 𝐵 ) ↑m 𝐵 ) ≈ ( 2om ( 𝐵 × 𝐵 ) ) ∧ ( 2om ( 𝐵 × 𝐵 ) ) ≈ ( 2om 𝐵 ) ) → ( ( 2om 𝐵 ) ↑m 𝐵 ) ≈ ( 2om 𝐵 ) )
19 11 17 18 syl2anc ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( ( 2om 𝐵 ) ↑m 𝐵 ) ≈ ( 2om 𝐵 ) )
20 3 ensymd ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( 2om 𝐵 ) ≈ 𝒫 𝐵 )
21 entr ( ( ( ( 2om 𝐵 ) ↑m 𝐵 ) ≈ ( 2om 𝐵 ) ∧ ( 2om 𝐵 ) ≈ 𝒫 𝐵 ) → ( ( 2om 𝐵 ) ↑m 𝐵 ) ≈ 𝒫 𝐵 )
22 19 20 21 syl2anc ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( ( 2om 𝐵 ) ↑m 𝐵 ) ≈ 𝒫 𝐵 )
23 domentr ( ( ( 𝐴m 𝐵 ) ≼ ( ( 2om 𝐵 ) ↑m 𝐵 ) ∧ ( ( 2om 𝐵 ) ↑m 𝐵 ) ≈ 𝒫 𝐵 ) → ( 𝐴m 𝐵 ) ≼ 𝒫 𝐵 )
24 7 22 23 syl2anc ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐴m 𝐵 ) ≼ 𝒫 𝐵 )
25 mapdom1 ( 2o𝐴 → ( 2om 𝐵 ) ≼ ( 𝐴m 𝐵 ) )
26 25 ad2antrl ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( 2om 𝐵 ) ≼ ( 𝐴m 𝐵 ) )
27 endomtr ( ( 𝒫 𝐵 ≈ ( 2om 𝐵 ) ∧ ( 2om 𝐵 ) ≼ ( 𝐴m 𝐵 ) ) → 𝒫 𝐵 ≼ ( 𝐴m 𝐵 ) )
28 3 26 27 syl2anc ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → 𝒫 𝐵 ≼ ( 𝐴m 𝐵 ) )
29 sbth ( ( ( 𝐴m 𝐵 ) ≼ 𝒫 𝐵 ∧ 𝒫 𝐵 ≼ ( 𝐴m 𝐵 ) ) → ( 𝐴m 𝐵 ) ≈ 𝒫 𝐵 )
30 24 28 29 syl2anc ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o𝐴𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐴m 𝐵 ) ≈ 𝒫 𝐵 )