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 𝐵 ) ≈ 𝒫 𝐵 )