Metamath Proof Explorer

Theorem r1pwcl

Description: The cumulative hierarchy of a limit ordinal is closed under power set. (Contributed by Raph Levien, 29-May-2004) (Proof shortened by Mario Carneiro, 17-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 r1elwf 
 |-  ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )
2 elfvdm 
 |-  ( A e. ( R1 ` B ) -> B e. dom R1 )
3 1 2 jca 
 |-  ( A e. ( R1 ` B ) -> ( A e. U. ( R1 " On ) /\ B e. dom R1 ) )
4 3 a1i 
 |-  ( Lim B -> ( A e. ( R1 ` B ) -> ( A e. U. ( R1 " On ) /\ B e. dom R1 ) ) )
5 r1elwf 
 |-  ( ~P A e. ( R1 ` B ) -> ~P A e. U. ( R1 " On ) )
6 pwwf 
 |-  ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) )
7 5 6 sylibr 
 |-  ( ~P A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )
8 elfvdm 
 |-  ( ~P A e. ( R1 ` B ) -> B e. dom R1 )
9 7 8 jca 
 |-  ( ~P A e. ( R1 ` B ) -> ( A e. U. ( R1 " On ) /\ B e. dom R1 ) )
10 9 a1i 
 |-  ( Lim B -> ( ~P A e. ( R1 ` B ) -> ( A e. U. ( R1 " On ) /\ B e. dom R1 ) ) )
11 limsuc 
 |-  ( Lim B -> ( ( rank ` A ) e. B <-> suc ( rank ` A ) e. B ) )
12 11 adantr 
 |-  ( ( Lim B /\ ( A e. U. ( R1 " On ) /\ B e. dom R1 ) ) -> ( ( rank ` A ) e. B <-> suc ( rank ` A ) e. B ) )
13 rankpwi 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` ~P A ) = suc ( rank ` A ) )
14 13 ad2antrl 
 |-  ( ( Lim B /\ ( A e. U. ( R1 " On ) /\ B e. dom R1 ) ) -> ( rank ` ~P A ) = suc ( rank ` A ) )
15 14 eleq1d 
 |-  ( ( Lim B /\ ( A e. U. ( R1 " On ) /\ B e. dom R1 ) ) -> ( ( rank ` ~P A ) e. B <-> suc ( rank ` A ) e. B ) )
16 12 15 bitr4d 
 |-  ( ( Lim B /\ ( A e. U. ( R1 " On ) /\ B e. dom R1 ) ) -> ( ( rank ` A ) e. B <-> ( rank ` ~P A ) e. B ) )
17 rankr1ag 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )
18 17 adantl 
 |-  ( ( Lim B /\ ( A e. U. ( R1 " On ) /\ B e. dom R1 ) ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )
19 rankr1ag 
 |-  ( ( ~P A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ~P A e. ( R1 ` B ) <-> ( rank ` ~P A ) e. B ) )
20 6 19 sylanb 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ~P A e. ( R1 ` B ) <-> ( rank ` ~P A ) e. B ) )
21 20 adantl 
 |-  ( ( Lim B /\ ( A e. U. ( R1 " On ) /\ B e. dom R1 ) ) -> ( ~P A e. ( R1 ` B ) <-> ( rank ` ~P A ) e. B ) )
22 16 18 21 3bitr4d 
 |-  ( ( Lim B /\ ( A e. U. ( R1 " On ) /\ B e. dom R1 ) ) -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` B ) ) )
23 22 ex 
 |-  ( Lim B -> ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` B ) ) ) )
24 4 10 23 pm5.21ndd 
 |-  ( Lim B -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` B ) ) )