Theorem hfpw

Description: The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015)

	Ref	Expression
Assertion	hfpw	⊢ ( 𝐴 ∈ Hf → 𝒫 𝐴 ∈ Hf )

Proof

Step	Hyp	Ref	Expression
1		rankpwg	⊢ ( 𝐴 ∈ Hf → ( rank ‘ 𝒫 𝐴 ) = suc ( rank ‘ 𝐴 ) )
2		elhf2g	⊢ ( 𝐴 ∈ Hf → ( 𝐴 ∈ Hf ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
3	2	ibi	⊢ ( 𝐴 ∈ Hf → ( rank ‘ 𝐴 ) ∈ ω )
4		peano2	⊢ ( ( rank ‘ 𝐴 ) ∈ ω → suc ( rank ‘ 𝐴 ) ∈ ω )
5	3 4	syl	⊢ ( 𝐴 ∈ Hf → suc ( rank ‘ 𝐴 ) ∈ ω )
6	1 5	eqeltrd	⊢ ( 𝐴 ∈ Hf → ( rank ‘ 𝒫 𝐴 ) ∈ ω )
7		pwexg	⊢ ( 𝐴 ∈ Hf → 𝒫 𝐴 ∈ V )
8		elhf2g	⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∈ Hf ↔ ( rank ‘ 𝒫 𝐴 ) ∈ ω ) )
9	7 8	syl	⊢ ( 𝐴 ∈ Hf → ( 𝒫 𝐴 ∈ Hf ↔ ( rank ‘ 𝒫 𝐴 ) ∈ ω ) )
10	6 9	mpbird	⊢ ( 𝐴 ∈ Hf → 𝒫 𝐴 ∈ Hf )