Metamath Proof Explorer

Theorem hfpw

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

Ref Expression
Assertion hfpw ⊢ A ∈ Hf → 𝒫 A ∈ Hf

Proof

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