Metamath Proof Explorer

Theorem ranklim

Description: The rank of a set belongs to a limit ordinal iff the rank of its power set does. (Contributed by NM, 18-Sep-2006)

Ref Expression
Assertion ranklim 
|- ( Lim B -> ( ( rank ` A ) e. B <-> ( rank ` ~P A ) e. B ) )

Proof

Step Hyp Ref Expression
1 limsuc 
 |-  ( Lim B -> ( ( rank ` A ) e. B <-> suc ( rank ` A ) e. B ) )
2 1 adantl 
 |-  ( ( A e. _V /\ Lim B ) -> ( ( rank ` A ) e. B <-> suc ( rank ` A ) e. B ) )
3 pweq 
 |-  ( x = A -> ~P x = ~P A )
4 3 fveq2d 
 |-  ( x = A -> ( rank ` ~P x ) = ( rank ` ~P A ) )
5 fveq2 
 |-  ( x = A -> ( rank ` x ) = ( rank ` A ) )
6 suceq 
 |-  ( ( rank ` x ) = ( rank ` A ) -> suc ( rank ` x ) = suc ( rank ` A ) )
7 5 6 syl 
 |-  ( x = A -> suc ( rank ` x ) = suc ( rank ` A ) )
8 4 7 eqeq12d 
 |-  ( x = A -> ( ( rank ` ~P x ) = suc ( rank ` x ) <-> ( rank ` ~P A ) = suc ( rank ` A ) ) )
9 vex 
 |-  x e. _V
10 9 rankpw 
 |-  ( rank ` ~P x ) = suc ( rank ` x )
11 8 10 vtoclg 
 |-  ( A e. _V -> ( rank ` ~P A ) = suc ( rank ` A ) )
12 11 eleq1d 
 |-  ( A e. _V -> ( ( rank ` ~P A ) e. B <-> suc ( rank ` A ) e. B ) )
13 12 adantr 
 |-  ( ( A e. _V /\ Lim B ) -> ( ( rank ` ~P A ) e. B <-> suc ( rank ` A ) e. B ) )
14 2 13 bitr4d 
 |-  ( ( A e. _V /\ Lim B ) -> ( ( rank ` A ) e. B <-> ( rank ` ~P A ) e. B ) )
15 fvprc 
 |-  ( -. A e. _V -> ( rank ` A ) = (/) )
16 pwexb 
 |-  ( A e. _V <-> ~P A e. _V )
17 fvprc 
 |-  ( -. ~P A e. _V -> ( rank ` ~P A ) = (/) )
18 16 17 sylnbi 
 |-  ( -. A e. _V -> ( rank ` ~P A ) = (/) )
19 15 18 eqtr4d 
 |-  ( -. A e. _V -> ( rank ` A ) = ( rank ` ~P A ) )
20 19 eleq1d 
 |-  ( -. A e. _V -> ( ( rank ` A ) e. B <-> ( rank ` ~P A ) e. B ) )
21 20 adantr 
 |-  ( ( -. A e. _V /\ Lim B ) -> ( ( rank ` A ) e. B <-> ( rank ` ~P A ) e. B ) )
22 14 21 pm2.61ian 
 |-  ( Lim B -> ( ( rank ` A ) e. B <-> ( rank ` ~P A ) e. B ) )