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		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
11	10	simpri	⊢ Lim dom 𝑅1
12		limsuc	⊢ ( Lim dom 𝑅1 → ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) )
13	11 12	ax-mp	⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
14	3 13	mpbi	⊢ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1
15		r1sucg	⊢ ( suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 → ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
16	14 15	ax-mp	⊢ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) )
17	9 16	eleqtrrdi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) )
18		r1elwf	⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) → 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
19	17 18	syl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
20		r1elssi	⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
21		pwexr	⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ V )
22		pwidg	⊢ ( 𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴 )
23	21 22	syl	⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ 𝒫 𝐴 )
24	20 23	sseldd	⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
25	19 24	impbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )