Theorem rankxpl

Description: A lower 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	rankxpl	|- ( ( A X. B ) =/= (/) -> ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		rankxpl.1	|- A e. _V
2		rankxpl.2	|- B e. _V
3		unixp	|- ( ( A X. B ) =/= (/) -> U. U. ( A X. B ) = ( A u. B ) )
4	3	fveq2d	|- ( ( A X. B ) =/= (/) -> ( rank ` U. U. ( A X. B ) ) = ( rank ` ( A u. B ) ) )
5	1 2	xpex	|- ( A X. B ) e. _V
6	5	uniex	|- U. ( A X. B ) e. _V
7	6	rankuniss	|- ( rank ` U. U. ( A X. B ) ) C_ ( rank ` U. ( A X. B ) )
8	5	rankuniss	|- ( rank ` U. ( A X. B ) ) C_ ( rank ` ( A X. B ) )
9	7 8	sstri	|- ( rank ` U. U. ( A X. B ) ) C_ ( rank ` ( A X. B ) )
10	4 9	eqsstrrdi	|- ( ( A X. B ) =/= (/) -> ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) )