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	$⊢ ((B \in dom card \land ω ≼ B) \land (2_{𝑜} ≼ A \land A ≼ 𝒫 B)) \to (A^{B}) \approx 𝒫 B$

Proof

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

Metamath Proof Explorer

Theorem mappwen

Proof