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	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		r1rankidb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
2	1	sspwd	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
3		rankdmr1	⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1
4		r1sucg	⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
5	3 4	ax-mp	⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) )
6	2 5	sseqtrrdi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
7		fvex	⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∈ V
8	7	elpw2	⊢ ( 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ↔ 𝒫 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
9	6 8	sylibr	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
10		r1dmlim	⊢ Lim dom 𝑅1
11		limsuc	⊢ ( Lim dom 𝑅1 → ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) )
12	10 11	ax-mp	⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
13	3 12	mpbi	⊢ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1
14		r1sucg	⊢ ( suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 → ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
15	13 14	ax-mp	⊢ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) )
16	9 15	eleqtrrdi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) )
17		r1elwf	⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) → 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
18	16 17	syl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
19		r1elssi	⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
20		pwexr	⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ V )
21		pwidg	⊢ ( 𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴 )
22	20 21	syl	⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ 𝒫 𝐴 )
23	19 22	sseldd	⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
24	18 23	impbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )