Theorem rankxpu

Description: An upper bound on the rank of a Cartesian product. (Contributed by NM, 18-Sep-2006)

	Ref	Expression
Hypotheses	rankxpl.1	$$⊢A\in \mathrm{V}$$
	rankxpl.2	$$⊢B\in \mathrm{V}$$
Assertion	rankxpu	$$⊢\mathrm{rank}\left(A\times B\right)\subseteq \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		xpsspw	$$⊢A\times B\subseteq 𝒫𝒫\left(A\cup B\right)$$
4	1 2	unex	$$⊢A\cup B\in \mathrm{V}$$
5	4	pwex	$$⊢𝒫\left(A\cup B\right)\in \mathrm{V}$$
6	5	pwex	$$⊢𝒫𝒫\left(A\cup B\right)\in \mathrm{V}$$
7	6	rankss	$$⊢A\times B\subseteq 𝒫𝒫\left(A\cup B\right)\to \mathrm{rank}\left(A\times B\right)\subseteq \mathrm{rank}\left(𝒫𝒫\left(A\cup B\right)\right)$$
8	3 7	ax-mp	$$⊢\mathrm{rank}\left(A\times B\right)\subseteq \mathrm{rank}\left(𝒫𝒫\left(A\cup B\right)\right)$$
9	5	rankpw	$$⊢\mathrm{rank}\left(𝒫𝒫\left(A\cup B\right)\right)=\mathrm{suc}\mathrm{rank}\left(𝒫\left(A\cup B\right)\right)$$
10	4	rankpw	$$⊢\mathrm{rank}\left(𝒫\left(A\cup B\right)\right)=\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
11		suceq	$$⊢\mathrm{rank}\left(𝒫\left(A\cup B\right)\right)=\mathrm{suc}\mathrm{rank}\left(A\cup B\right)\to \mathrm{suc}\mathrm{rank}\left(𝒫\left(A\cup B\right)\right)=\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
12	10 11	ax-mp	$$⊢\mathrm{suc}\mathrm{rank}\left(𝒫\left(A\cup B\right)\right)=\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
13	9 12	eqtri	$$⊢\mathrm{rank}\left(𝒫𝒫\left(A\cup B\right)\right)=\mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$
14	8 13	sseqtri	$$⊢\mathrm{rank}\left(A\times B\right)\subseteq \mathrm{suc}\mathrm{suc}\mathrm{rank}\left(A\cup B\right)$$