Theorem hfrn

Description: The range of a hereditarily finite set is hereditarily finite. (Contributed by Eric Schmidt, 26-Sep-2026)

	Ref	Expression
Assertion	hfrn	|- ( A e. HF -> ran A e. HF )

Proof

Step	Hyp	Ref	Expression
1		hfuni	|- ( A e. HF -> U. A e. HF )
2		hfuni	|- ( U. A e. HF -> U. U. A e. HF )
3		ssun2	|- ran A C_ ( dom A u. ran A )
4		dmrnssfld	|- ( dom A u. ran A ) C_ U. U. A
5	3 4	sstri	|- ran A C_ U. U. A
6		hfsshf	|- ( ( ran A C_ U. U. A /\ U. U. A e. HF ) -> ran A e. HF )
7	5 6	mpan	|- ( U. U. A e. HF -> ran A e. HF )
8	1 2 7	3syl	|- ( A e. HF -> ran A e. HF )