Metamath Proof Explorer

Theorem rankpwi

Description: The rank of a power set. Part of Exercise 30 of Enderton p. 207. (Contributed by Mario Carneiro, 3-Jun-2013)

Ref Expression
Assertion rankpwi 
|- ( A e. U. ( R1 " On ) -> ( rank ` ~P A ) = suc ( rank ` A ) )

Proof

Step Hyp Ref Expression
1 rankidn 
 |-  ( A e. U. ( R1 " On ) -> -. A e. ( R1 ` ( rank ` A ) ) )
2 rankon 
 |-  ( rank ` A ) e. On
3 r1suc 
 |-  ( ( rank ` A ) e. On -> ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) )
4 2 3 ax-mp 
 |-  ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) )
5 4 eleq2i 
 |-  ( ~P A e. ( R1 ` suc ( rank ` A ) ) <-> ~P A e. ~P ( R1 ` ( rank ` A ) ) )
6 elpwi 
 |-  ( ~P A e. ~P ( R1 ` ( rank ` A ) ) -> ~P A C_ ( R1 ` ( rank ` A ) ) )
7 pwidg 
 |-  ( A e. U. ( R1 " On ) -> A e. ~P A )
8 ssel 
 |-  ( ~P A C_ ( R1 ` ( rank ` A ) ) -> ( A e. ~P A -> A e. ( R1 ` ( rank ` A ) ) ) )
9 6 7 8 syl2imc 
 |-  ( A e. U. ( R1 " On ) -> ( ~P A e. ~P ( R1 ` ( rank ` A ) ) -> A e. ( R1 ` ( rank ` A ) ) ) )
10 5 9 biimtrid 
 |-  ( A e. U. ( R1 " On ) -> ( ~P A e. ( R1 ` suc ( rank ` A ) ) -> A e. ( R1 ` ( rank ` A ) ) ) )
11 1 10 mtod 
 |-  ( A e. U. ( R1 " On ) -> -. ~P A e. ( R1 ` suc ( rank ` A ) ) )
12 r1rankidb 
 |-  ( A e. U. ( R1 " On ) -> A C_ ( R1 ` ( rank ` A ) ) )
13 12 sspwd 
 |-  ( A e. U. ( R1 " On ) -> ~P A C_ ~P ( R1 ` ( rank ` A ) ) )
14 13 4 sseqtrrdi 
 |-  ( A e. U. ( R1 " On ) -> ~P A C_ ( R1 ` suc ( rank ` A ) ) )
15 fvex 
 |-  ( R1 ` suc ( rank ` A ) ) e. _V
16 15 elpw2 
 |-  ( ~P A e. ~P ( R1 ` suc ( rank ` A ) ) <-> ~P A C_ ( R1 ` suc ( rank ` A ) ) )
17 14 16 sylibr 
 |-  ( A e. U. ( R1 " On ) -> ~P A e. ~P ( R1 ` suc ( rank ` A ) ) )
18 2 onsuci 
 |-  suc ( rank ` A ) e. On
19 r1suc 
 |-  ( suc ( rank ` A ) e. On -> ( R1 ` suc suc ( rank ` A ) ) = ~P ( R1 ` suc ( rank ` A ) ) )
20 18 19 ax-mp 
 |-  ( R1 ` suc suc ( rank ` A ) ) = ~P ( R1 ` suc ( rank ` A ) )
21 17 20 eleqtrrdi 
 |-  ( A e. U. ( R1 " On ) -> ~P A e. ( R1 ` suc suc ( rank ` A ) ) )
22 pwwf 
 |-  ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) )
23 rankr1c 
 |-  ( ~P A e. U. ( R1 " On ) -> ( suc ( rank ` A ) = ( rank ` ~P A ) <-> ( -. ~P A e. ( R1 ` suc ( rank ` A ) ) /\ ~P A e. ( R1 ` suc suc ( rank ` A ) ) ) ) )
24 22 23 sylbi 
 |-  ( A e. U. ( R1 " On ) -> ( suc ( rank ` A ) = ( rank ` ~P A ) <-> ( -. ~P A e. ( R1 ` suc ( rank ` A ) ) /\ ~P A e. ( R1 ` suc suc ( rank ` A ) ) ) ) )
25 11 21 24 mpbir2and 
 |-  ( A e. U. ( R1 " On ) -> suc ( rank ` A ) = ( rank ` ~P A ) )
26 25 eqcomd 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` ~P A ) = suc ( rank ` A ) )