This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) )
3 2 ad2antrr ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) )
4 domentr ⊢ ( ( 𝐴 ≼ 𝒫 𝐵 ∧ 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) ) → 𝐴 ≼ ( 2o ↑m 𝐵 ) )
5 1 3 4 syl2anc ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → 𝐴 ≼ ( 2o ↑m 𝐵 ) )
6 mapdom1 ⊢ ( 𝐴 ≼ ( 2o ↑m 𝐵 ) → ( 𝐴 ↑m 𝐵 ) ≼ ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) )
7 5 6 syl ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐴 ↑m 𝐵 ) ≼ ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) )
8 2on ⊢ 2o ∈ On
9 simpll ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → 𝐵 ∈ dom card )
10 mapxpen ⊢ ( ( 2o ∈ On ∧ 𝐵 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ≈ ( 2o ↑m ( 𝐵 × 𝐵 ) ) )
11 8 9 9 10 mp3an2i ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ≈ ( 2o ↑m ( 𝐵 × 𝐵 ) ) )
12 8 elexi ⊢ 2o ∈ V
13 12 enref ⊢ 2o ≈ 2o
14 infxpidm2 ⊢ ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) → ( 𝐵 × 𝐵 ) ≈ 𝐵 )
15 14 adantr ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐵 × 𝐵 ) ≈ 𝐵 )
16 mapen ⊢ ( ( 2o ≈ 2o ∧ ( 𝐵 × 𝐵 ) ≈ 𝐵 ) → ( 2o ↑m ( 𝐵 × 𝐵 ) ) ≈ ( 2o ↑m 𝐵 ) )
17 13 15 16 sylancr ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( 2o ↑m ( 𝐵 × 𝐵 ) ) ≈ ( 2o ↑m 𝐵 ) )
18 entr ⊢ ( ( ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ≈ ( 2o ↑m ( 𝐵 × 𝐵 ) ) ∧ ( 2o ↑m ( 𝐵 × 𝐵 ) ) ≈ ( 2o ↑m 𝐵 ) ) → ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ≈ ( 2o ↑m 𝐵 ) )
19 11 17 18 syl2anc ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ≈ ( 2o ↑m 𝐵 ) )
20 3 ensymd ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 )
21 entr ⊢ ( ( ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ≈ ( 2o ↑m 𝐵 ) ∧ ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 ) → ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ≈ 𝒫 𝐵 )
22 19 20 21 syl2anc ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ≈ 𝒫 𝐵 )
23 domentr ⊢ ( ( ( 𝐴 ↑m 𝐵 ) ≼ ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ∧ ( ( 2o ↑m 𝐵 ) ↑m 𝐵 ) ≈ 𝒫 𝐵 ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 )
24 7 22 23 syl2anc ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 )
25 mapdom1 ⊢ ( 2o ≼ 𝐴 → ( 2o ↑m 𝐵 ) ≼ ( 𝐴 ↑m 𝐵 ) )
26 25 ad2antrl ⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( 2o ↑m 𝐵 ) ≼ ( 𝐴 ↑m 𝐵 ) )
27 endomtr ⊢ ( ( 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) ∧ ( 2o ↑m 𝐵 ) ≼ ( 𝐴 ↑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 𝐵 ) ≈ 𝒫 𝐵 )