hfpw

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

		Ref	Expression
	Assertion	hfpw	$⊢ A \in Hf \to 𝒫 A \in Hf$

Step	Hyp	Ref	Expression
1		rankpwg	$⊢ A \in Hf \to rank (𝒫 A) = suc rank (A)$
2		elhf2g	$⊢ A \in Hf \to (A \in Hf \leftrightarrow rank (A) \in ω)$
3	2	ibi	$⊢ A \in Hf \to rank (A) \in ω$
4		peano2	$⊢ rank (A) \in ω \to suc rank (A) \in ω$
5	3 4	syl	$⊢ A \in Hf \to suc rank (A) \in ω$
6	1 5	eqeltrd	$⊢ A \in Hf \to rank (𝒫 A) \in ω$
7		pwexg	$⊢ A \in Hf \to 𝒫 A \in V$
8		elhf2g	$⊢ 𝒫 A \in V \to (𝒫 A \in Hf \leftrightarrow rank (𝒫 A) \in ω)$
9	7 8	syl	$⊢ A \in Hf \to (𝒫 A \in Hf \leftrightarrow rank (𝒫 A) \in ω)$
10	6 9	mpbird	$⊢ A \in Hf \to 𝒫 A \in Hf$

Metamath Proof Explorer