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

Metamath Proof Explorer

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