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 e. HF -> A e. Fin )

Proof

Step	Hyp	Ref	Expression
1		df-hf	|- HF = U. ( R1 " _om )
2	1	eleq2i	|- ( A e. HF <-> A e. U. ( R1 " _om ) )
3		r1fun	|- Fun R1
4		eluniima	|- ( Fun R1 -> ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) ) )
5	3 4	ax-mp	|- ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) )
6	2 5	sylbb	|- ( A e. HF -> E. x e. _om A e. ( R1 ` x ) )
7		r1fin	|- ( x e. _om -> ( R1 ` x ) e. Fin )
8		r1pwss	|- ( A e. ( R1 ` x ) -> ~P A C_ ( R1 ` x ) )
9		ssfi	|- ( ( ( R1 ` x ) e. Fin /\ ~P A C_ ( R1 ` x ) ) -> ~P A e. Fin )
10	7 8 9	syl2an	|- ( ( x e. _om /\ A e. ( R1 ` x ) ) -> ~P A e. Fin )
11	10	rexlimiva	|- ( E. x e. _om A e. ( R1 ` x ) -> ~P A e. Fin )
12		pwfir	|- ( ~P A e. Fin -> A e. Fin )
13	6 11 12	3syl	|- ( A e. HF -> A e. Fin )