Theorem hfpwOLD

Description: Obsolete version of hfpw as of 17-Sep-2026. (Contributed by Scott Fenton, 16-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hfpwOLD	⊢ ( 𝐴 ∈ 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 )