Metamath Proof Explorer

Theorem rankmapu

Description: An upper bound on the rank of set exponentiation. (Contributed by Gérard Lang, 5-Aug-2018)

Ref Expression
Hypotheses rankxpl.1 
|- A e. _V
rankxpl.2 
|- B e. _V
Assertion rankmapu 
|- ( rank ` ( A ^m B ) ) C_ suc suc suc ( rank ` ( A u. B ) )

Proof

Step Hyp Ref Expression
1 rankxpl.1 
 |-  A e. _V
2 rankxpl.2 
 |-  B e. _V
3 mapsspw 
 |-  ( A ^m B ) C_ ~P ( B X. A )
4 2 1 xpex 
 |-  ( B X. A ) e. _V
5 4 pwex 
 |-  ~P ( B X. A ) e. _V
6 5 rankss 
 |-  ( ( A ^m B ) C_ ~P ( B X. A ) -> ( rank ` ( A ^m B ) ) C_ ( rank ` ~P ( B X. A ) ) )
7 3 6 ax-mp 
 |-  ( rank ` ( A ^m B ) ) C_ ( rank ` ~P ( B X. A ) )
8 4 rankpw 
 |-  ( rank ` ~P ( B X. A ) ) = suc ( rank ` ( B X. A ) )
9 2 1 rankxpu 
 |-  ( rank ` ( B X. A ) ) C_ suc suc ( rank ` ( B u. A ) )
10 uncom 
 |-  ( B u. A ) = ( A u. B )
11 10 fveq2i 
 |-  ( rank ` ( B u. A ) ) = ( rank ` ( A u. B ) )
12 suceq 
 |-  ( ( rank ` ( B u. A ) ) = ( rank ` ( A u. B ) ) -> suc ( rank ` ( B u. A ) ) = suc ( rank ` ( A u. B ) ) )
13 11 12 ax-mp 
 |-  suc ( rank ` ( B u. A ) ) = suc ( rank ` ( A u. B ) )
14 suceq 
 |-  ( suc ( rank ` ( B u. A ) ) = suc ( rank ` ( A u. B ) ) -> suc suc ( rank ` ( B u. A ) ) = suc suc ( rank ` ( A u. B ) ) )
15 13 14 ax-mp 
 |-  suc suc ( rank ` ( B u. A ) ) = suc suc ( rank ` ( A u. B ) )
16 9 15 sseqtri 
 |-  ( rank ` ( B X. A ) ) C_ suc suc ( rank ` ( A u. B ) )
17 rankon 
 |-  ( rank ` ( B X. A ) ) e. On
18 17 onordi 
 |-  Ord ( rank ` ( B X. A ) )
19 rankon 
 |-  ( rank ` ( A u. B ) ) e. On
20 19 onsuci 
 |-  suc ( rank ` ( A u. B ) ) e. On
21 20 onsuci 
 |-  suc suc ( rank ` ( A u. B ) ) e. On
22 21 onordi 
 |-  Ord suc suc ( rank ` ( A u. B ) )
23 ordsucsssuc 
 |-  ( ( Ord ( rank ` ( B X. A ) ) /\ Ord suc suc ( rank ` ( A u. B ) ) ) -> ( ( rank ` ( B X. A ) ) C_ suc suc ( rank ` ( A u. B ) ) <-> suc ( rank ` ( B X. A ) ) C_ suc suc suc ( rank ` ( A u. B ) ) ) )
24 18 22 23 mp2an 
 |-  ( ( rank ` ( B X. A ) ) C_ suc suc ( rank ` ( A u. B ) ) <-> suc ( rank ` ( B X. A ) ) C_ suc suc suc ( rank ` ( A u. B ) ) )
25 16 24 mpbi 
 |-  suc ( rank ` ( B X. A ) ) C_ suc suc suc ( rank ` ( A u. B ) )
26 8 25 eqsstri 
 |-  ( rank ` ~P ( B X. A ) ) C_ suc suc suc ( rank ` ( A u. B ) )
27 7 26 sstri 
 |-  ( rank ` ( A ^m B ) ) C_ suc suc suc ( rank ` ( A u. B ) )