This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
11 10 simpri 
 |-  Lim dom R1
12 limsuc 
 |-  ( Lim dom R1 -> ( ( rank ` A ) e. dom R1 <-> suc ( rank ` A ) e. dom R1 ) )
13 11 12 ax-mp 
 |-  ( ( rank ` A ) e. dom R1 <-> suc ( rank ` A ) e. dom R1 )
14 3 13 mpbi 
 |-  suc ( rank ` A ) e. dom R1
15 r1sucg 
 |-  ( suc ( rank ` A ) e. dom R1 -> ( R1 ` suc suc ( rank ` A ) ) = ~P ( R1 ` suc ( rank ` A ) ) )
16 14 15 ax-mp 
 |-  ( R1 ` suc suc ( rank ` A ) ) = ~P ( R1 ` suc ( rank ` A ) )
17 9 16 eleqtrrdi 
 |-  ( A e. U. ( R1 " On ) -> ~P A e. ( R1 ` suc suc ( rank ` A ) ) )
18 r1elwf 
 |-  ( ~P A e. ( R1 ` suc suc ( rank ` A ) ) -> ~P A e. U. ( R1 " On ) )
19 17 18 syl 
 |-  ( A e. U. ( R1 " On ) -> ~P A e. U. ( R1 " On ) )
20 r1elssi 
 |-  ( ~P A e. U. ( R1 " On ) -> ~P A C_ U. ( R1 " On ) )
21 pwexr 
 |-  ( ~P A e. U. ( R1 " On ) -> A e. _V )
22 pwidg 
 |-  ( A e. _V -> A e. ~P A )
23 21 22 syl 
 |-  ( ~P A e. U. ( R1 " On ) -> A e. ~P A )
24 20 23 sseldd 
 |-  ( ~P A e. U. ( R1 " On ) -> A e. U. ( R1 " On ) )
25 19 24 impbii 
 |-  ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) )