Theorem rankmapu

Description: An upper bound on the rank of set exponentiation. (Contributed by Gérard Lang, 5-Aug-2018)

	Ref	Expression
Hypotheses	rankxpl.1	$$⊢A\in \mathrm{V}$$
	rankxpl.2	$$⊢B\in \mathrm{V}$$
Assertion	rankmapu	$$⊢\mathrm{rank}\left(A^B\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rankxpl.1	$$⊢A\in \mathrm{V}$$
2		rankxpl.2	$$⊢B\in \mathrm{V}$$
3		mapsspw	$$⊢A^B\subseteq 𝒫\left(B\times A\right)$$
4	2 1	xpex	$$⊢B\times A\in \mathrm{V}$$
5	4	pwex	$$⊢𝒫\left(B\times A\right)\in \mathrm{V}$$
6	5	rankss	$$⊢A^B\subseteq 𝒫\left(B\times A\right)\to \mathrm{rank}\left(A^B\right)\subseteq \mathrm{rank}\left(𝒫\left(B\times A\right)\right)$$
7	3 6	ax-mp	$$⊢\mathrm{rank}\left(A^B\right)\subseteq \mathrm{rank}\left(𝒫\left(B\times A\right)\right)$$
8	4	rankpw	$$⊢\mathrm{rank}\left(𝒫\left(B\times A\right)\right)=\mathrm{suc}\mathrm{rank}\left(B\times A\right)$$
9	2 1	rankxpu	$$⊢\mathrm{rank}\left(B\times A\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{rank}\left(B\cup A\right)$$
10		uncom	$$⊢B\cup A=A\cup B$$
11	10	fveq2i	$$⊢\mathrm{rank}\left(B\cup A\right)=\mathrm{rank}\left(A\cup B\right)$$
12		suceq	$$⊢\mathrm{rank}\left(B\cup A\right)=\mathrm{rank}\left(A\cup B\right)\to \mathrm{suc}\mathrm{rank}\left(B\cup A\right)=\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
13	11 12	ax-mp	$$⊢\mathrm{suc}\mathrm{rank}\left(B\cup A\right)=\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
14		suceq	$$⊢\mathrm{suc}\mathrm{rank}\left(B\cup A\right)=\mathrm{suc}\mathrm{rank}\left(A\cup B\right)\to \mathrm{suc}\mathrm{suc}\mathrm{rank}\left(B\cup A\right)=\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
15	13 14	ax-mp	$$⊢\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(B\cup A\right)=\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
16	9 15	sseqtri	$$⊢\mathrm{rank}\left(B\times A\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
17		rankon	$$⊢\mathrm{rank}\left(B\times A\right)\in \mathrm{On}$$
18	17	onordi	$$⊢\mathrm{Ord}\mathrm{rank}\left(B\times A\right)$$
19		rankon	$$⊢\mathrm{rank}\left(A\cup B\right)\in \mathrm{On}$$
20	19	onsuci	$$⊢\mathrm{suc}\mathrm{rank}\left(A\cup B\right)\in \mathrm{On}$$
21	20	onsuci	$$⊢\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)\in \mathrm{On}$$
22	21	onordi	$$⊢\mathrm{Ord}\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
23		ordsucsssuc	$$⊢\left(\mathrm{Ord}\mathrm{rank}\left(B\times A\right)\wedge \mathrm{Ord}\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)\right)\to \left(\mathrm{rank}\left(B\times A\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)\leftrightarrow \mathrm{suc}\mathrm{rank}\left(B\times A\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)\right)$$
24	18 22 23	mp2an	$$⊢\mathrm{rank}\left(B\times A\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)\leftrightarrow \mathrm{suc}\mathrm{rank}\left(B\times A\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
25	16 24	mpbi	$$⊢\mathrm{suc}\mathrm{rank}\left(B\times A\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
26	8 25	eqsstri	$$⊢\mathrm{rank}\left(𝒫\left(B\times A\right)\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
27	7 26	sstri	$$⊢\mathrm{rank}\left(A^B\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$