This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )