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		r1funlim	|- ( Fun R1 /\ Lim dom R1 )
4	3	simpli	|- Fun R1
5		eluniima	|- ( Fun R1 -> ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) ) )
6	4 5	ax-mp	|- ( A e. U. ( R1 " _om ) <-> E. x e. _om A e. ( R1 ` x ) )
7	2 6	sylbb	|- ( A e. Hf -> E. x e. _om A e. ( R1 ` x ) )
8		r1fin	|- ( x e. _om -> ( R1 ` x ) e. Fin )
9		r1pwss	|- ( A e. ( R1 ` x ) -> ~P A C_ ( R1 ` x ) )
10		ssfi	|- ( ( ( R1 ` x ) e. Fin /\ ~P A C_ ( R1 ` x ) ) -> ~P A e. Fin )
11	8 9 10	syl2an	|- ( ( x e. _om /\ A e. ( R1 ` x ) ) -> ~P A e. Fin )
12	11	rexlimiva	|- ( E. x e. _om A e. ( R1 ` x ) -> ~P A e. Fin )
13		pwfir	|- ( ~P A e. Fin -> A e. Fin )
14	7 12 13	3syl	|- ( A e. Hf -> A e. Fin )