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 e. _V
	rankxpl.2	|- B e. _V
Assertion	rankxpu	|- ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) )

Proof

Step	Hyp	Ref	Expression
1		rankxpl.1	|- A e. _V
2		rankxpl.2	|- B e. _V
3		xpsspw	|- ( A X. B ) C_ ~P ~P ( A u. B )
4	1 2	unex	|- ( A u. B ) e. _V
5	4	pwex	|- ~P ( A u. B ) e. _V
6	5	pwex	|- ~P ~P ( A u. B ) e. _V
7	6	rankss	|- ( ( A X. B ) C_ ~P ~P ( A u. B ) -> ( rank ` ( A X. B ) ) C_ ( rank ` ~P ~P ( A u. B ) ) )
8	3 7	ax-mp	|- ( rank ` ( A X. B ) ) C_ ( rank ` ~P ~P ( A u. B ) )
9	5	rankpw	|- ( rank ` ~P ~P ( A u. B ) ) = suc ( rank ` ~P ( A u. B ) )
10	4	rankpw	|- ( rank ` ~P ( A u. B ) ) = suc ( rank ` ( A u. B ) )
11		suceq	|- ( ( rank ` ~P ( A u. B ) ) = suc ( rank ` ( A u. B ) ) -> suc ( rank ` ~P ( A u. B ) ) = suc suc ( rank ` ( A u. B ) ) )
12	10 11	ax-mp	|- suc ( rank ` ~P ( A u. B ) ) = suc suc ( rank ` ( A u. B ) )
13	9 12	eqtri	|- ( rank ` ~P ~P ( A u. B ) ) = suc suc ( rank ` ( A u. B ) )
14	8 13	sseqtri	|- ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) )