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