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