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 ) )