Metamath Proof Explorer

Theorem pwwf

Description: A power set is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion pwwf 
|- ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 r1rankidb 
 |-  ( A e. U. ( R1 " On ) -> A C_ ( R1 ` ( rank ` A ) ) )
2 1 sspwd 
 |-  ( A e. U. ( R1 " On ) -> ~P A C_ ~P ( R1 ` ( rank ` A ) ) )
3 rankdmr1 
 |-  ( rank ` A ) e. dom R1
4 r1sucg 
 |-  ( ( rank ` A ) e. dom R1 -> ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) )
5 3 4 ax-mp 
 |-  ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) )
6 2 5 sseqtrrdi 
 |-  ( A e. U. ( R1 " On ) -> ~P A C_ ( R1 ` suc ( rank ` A ) ) )
7 fvex 
 |-  ( R1 ` suc ( rank ` A ) ) e. _V
8 7 elpw2 
 |-  ( ~P A e. ~P ( R1 ` suc ( rank ` A ) ) <-> ~P A C_ ( R1 ` suc ( rank ` A ) ) )
9 6 8 sylibr 
 |-  ( A e. U. ( R1 " On ) -> ~P A e. ~P ( R1 ` suc ( rank ` A ) ) )
10 r1dmlim 
 |-  Lim dom R1
11 limsuc 
 |-  ( Lim dom R1 -> ( ( rank ` A ) e. dom R1 <-> suc ( rank ` A ) e. dom R1 ) )
12 10 11 ax-mp 
 |-  ( ( rank ` A ) e. dom R1 <-> suc ( rank ` A ) e. dom R1 )
13 3 12 mpbi 
 |-  suc ( rank ` A ) e. dom R1
14 r1sucg 
 |-  ( suc ( rank ` A ) e. dom R1 -> ( R1 ` suc suc ( rank ` A ) ) = ~P ( R1 ` suc ( rank ` A ) ) )
15 13 14 ax-mp 
 |-  ( R1 ` suc suc ( rank ` A ) ) = ~P ( R1 ` suc ( rank ` A ) )
16 9 15 eleqtrrdi 
 |-  ( A e. U. ( R1 " On ) -> ~P A e. ( R1 ` suc suc ( rank ` A ) ) )
17 r1elwf 
 |-  ( ~P A e. ( R1 ` suc suc ( rank ` A ) ) -> ~P A e. U. ( R1 " On ) )
18 16 17 syl 
 |-  ( A e. U. ( R1 " On ) -> ~P A e. U. ( R1 " On ) )
19 r1elssi 
 |-  ( ~P A e. U. ( R1 " On ) -> ~P A C_ U. ( R1 " On ) )
20 pwexr 
 |-  ( ~P A e. U. ( R1 " On ) -> A e. _V )
21 pwidg 
 |-  ( A e. _V -> A e. ~P A )
22 20 21 syl 
 |-  ( ~P A e. U. ( R1 " On ) -> A e. ~P A )
23 19 22 sseldd 
 |-  ( ~P A e. U. ( R1 " On ) -> A e. U. ( R1 " On ) )
24 18 23 impbii 
 |-  ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) )