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	Could not format assertion : No typesetting found for |- ( A e. HF -> A e. Fin ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-hf	Could not format HF = U. ( R1 " _om ) : No typesetting found for |- HF = U. ( R1 " _om ) with typecode |-
2	1	eleq2i	Could not format ( A e. HF <-> A e. U. ( R1 " _om ) ) : No typesetting found for |- ( A e. HF <-> A e. U. ( R1 " _om ) ) with typecode |-
3		r1fun	$$⊢\mathrm{Fun}{R}_1$$
4		eluniima	$$⊢\mathrm{Fun}{R}_1\to \left(A\in \bigcup R_1\left[\mathrm{\omega }\right]\leftrightarrow \exists x\in \mathrm{\omega }A\in R_1\left(x\right)\right)$$
5	3 4	ax-mp	$$⊢A\in \bigcup R_1\left[\mathrm{\omega }\right]\leftrightarrow \exists x\in \mathrm{\omega }A\in R_1\left(x\right)$$
6	2 5	sylbb	Could not format ( A e. HF -> E. x e. _om A e. ( R1 ` x ) ) : No typesetting found for |- ( A e. HF -> E. x e. _om A e. ( R1 ` x ) ) with typecode |-
7		r1fin	$$⊢x\in \mathrm{\omega }\to R_1\left(x\right)\in \mathrm{Fin}$$
8		r1pwss	$$⊢A\in R_1\left(x\right)\to 𝒫A\subseteq R_1\left(x\right)$$
9		ssfi	$$⊢\left(R_1\left(x\right)\in \mathrm{Fin}\wedge 𝒫A\subseteq R_1\left(x\right)\right)\to 𝒫A\in \mathrm{Fin}$$
10	7 8 9	syl2an	$$⊢\left(x\in \mathrm{\omega }\wedge A\in R_1\left(x\right)\right)\to 𝒫A\in \mathrm{Fin}$$
11	10	rexlimiva	$$⊢\exists x\in \mathrm{\omega }A\in R_1\left(x\right)\to 𝒫A\in \mathrm{Fin}$$
12		pwfir	$$⊢𝒫A\in \mathrm{Fin}\to A\in \mathrm{Fin}$$
13	6 11 12	3syl	Could not format ( A e. HF -> A e. Fin ) : No typesetting found for |- ( A e. HF -> A e. Fin ) with typecode |-