Metamath Proof Explorer

Theorem hffi

Description: Hereditarily finite sets are finite sets. (Contributed by BTernaryTau, 30-Dec-2025) Restate using the defined Hf symbol. (Revised by Eric Schmidt, 8-Sep-2026)

		Ref	Expression
	Assertion	hffi	$⊢ A \in Hf \to A \in Fin$

Proof

Step	Hyp	Ref	Expression
1		df-hf	$⊢ Hf = ⋃ R_{1} [ω]$
2	1	eleq2i	$⊢ A \in Hf \leftrightarrow A \in ⋃ R_{1} [ω]$
3		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
4	3	simpli	$⊢ Fun R_{1}$
5		eluniima	$⊢ Fun R_{1} \to (A \in ⋃ R_{1} [ω] \leftrightarrow \exists x \in ω A \in R_{1} (x))$
6	4 5	ax-mp	$⊢ A \in ⋃ R_{1} [ω] \leftrightarrow \exists x \in ω A \in R_{1} (x)$
7	2 6	sylbb	$⊢ A \in Hf \to \exists x \in ω A \in R_{1} (x)$
8		r1fin	$⊢ x \in ω \to R_{1} (x) \in Fin$
9		r1pwss	$⊢ A \in R_{1} (x) \to 𝒫 A \subseteq R_{1} (x)$
10		ssfi	$⊢ (R_{1} (x) \in Fin \land 𝒫 A \subseteq R_{1} (x)) \to 𝒫 A \in Fin$
11	8 9 10	syl2an	$⊢ (x \in ω \land A \in R_{1} (x)) \to 𝒫 A \in Fin$
12	11	rexlimiva	$⊢ \exists x \in ω A \in R_{1} (x) \to 𝒫 A \in Fin$
13		pwfir	$⊢ 𝒫 A \in Fin \to A \in Fin$
14	7 12 13	3syl	$⊢ A \in Hf \to A \in Fin$