Metamath Proof Explorer

Theorem r1pw

Description: A stronger property of R1 than rankpw . The latter merely proves that R1 of the successor is a power set, but here we prove that if A is in the cumulative hierarchy, then ~P A is in the cumulative hierarchy of the successor. (Contributed by Raph Levien, 29-May-2004) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion r1pw 
|- ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )

Proof

Step Hyp Ref Expression
1 rankpwi 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` ~P A ) = suc ( rank ` A ) )
2 1 eleq1d 
 |-  ( A e. U. ( R1 " On ) -> ( ( rank ` ~P A ) e. suc B <-> suc ( rank ` A ) e. suc B ) )
3 eloni 
 |-  ( B e. On -> Ord B )
4 ordsucelsuc 
 |-  ( Ord B -> ( ( rank ` A ) e. B <-> suc ( rank ` A ) e. suc B ) )
5 3 4 syl 
 |-  ( B e. On -> ( ( rank ` A ) e. B <-> suc ( rank ` A ) e. suc B ) )
6 5 bicomd 
 |-  ( B e. On -> ( suc ( rank ` A ) e. suc B <-> ( rank ` A ) e. B ) )
7 2 6 sylan9bb 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. On ) -> ( ( rank ` ~P A ) e. suc B <-> ( rank ` A ) e. B ) )
8 pwwf 
 |-  ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) )
9 8 biimpi 
 |-  ( A e. U. ( R1 " On ) -> ~P A e. U. ( R1 " On ) )
10 suceloni 
 |-  ( B e. On -> suc B e. On )
11 r1fnon 
 |-  R1 Fn On
12 11 fndmi 
 |-  dom R1 = On
13 10 12 eleqtrrdi 
 |-  ( B e. On -> suc B e. dom R1 )
14 rankr1ag 
 |-  ( ( ~P A e. U. ( R1 " On ) /\ suc B e. dom R1 ) -> ( ~P A e. ( R1 ` suc B ) <-> ( rank ` ~P A ) e. suc B ) )
15 9 13 14 syl2an 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. On ) -> ( ~P A e. ( R1 ` suc B ) <-> ( rank ` ~P A ) e. suc B ) )
16 12 eleq2i 
 |-  ( B e. dom R1 <-> B e. On )
17 rankr1ag 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )
18 16 17 sylan2br 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. On ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )
19 7 15 18 3bitr4rd 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. On ) -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )
20 19 ex 
 |-  ( A e. U. ( R1 " On ) -> ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) ) )
21 r1elwf 
 |-  ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )
22 r1elwf 
 |-  ( ~P A e. ( R1 ` suc B ) -> ~P A e. U. ( R1 " On ) )
23 r1elssi 
 |-  ( ~P A e. U. ( R1 " On ) -> ~P A C_ U. ( R1 " On ) )
24 22 23 syl 
 |-  ( ~P A e. ( R1 ` suc B ) -> ~P A C_ U. ( R1 " On ) )
25 ssid 
 |-  A C_ A
26 pwexr 
 |-  ( ~P A e. ( R1 ` suc B ) -> A e. _V )
27 elpwg 
 |-  ( A e. _V -> ( A e. ~P A <-> A C_ A ) )
28 26 27 syl 
 |-  ( ~P A e. ( R1 ` suc B ) -> ( A e. ~P A <-> A C_ A ) )
29 25 28 mpbiri 
 |-  ( ~P A e. ( R1 ` suc B ) -> A e. ~P A )
30 24 29 sseldd 
 |-  ( ~P A e. ( R1 ` suc B ) -> A e. U. ( R1 " On ) )
31 21 30 pm5.21ni 
 |-  ( -. A e. U. ( R1 " On ) -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )
32 31 a1d 
 |-  ( -. A e. U. ( R1 " On ) -> ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) ) )
33 20 32 pm2.61i 
 |-  ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )