Theorem hfrn

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

	Ref	Expression
Assertion	hfrn	⊢ ( 𝐴 ∈ HF → ran 𝐴 ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		hfuni	⊢ ( 𝐴 ∈ HF → ∪ 𝐴 ∈ HF )
2		hfuni	⊢ ( ∪ 𝐴 ∈ HF → ∪ ∪ 𝐴 ∈ HF )
3		ssun2	⊢ ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
4		dmrnssfld	⊢ ( dom 𝐴 ∪ ran 𝐴 ) ⊆ ∪ ∪ 𝐴
5	3 4	sstri	⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		hfsshf	⊢ ( ( ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ HF ) → ran 𝐴 ∈ HF )
7	5 6	mpan	⊢ ( ∪ ∪ 𝐴 ∈ HF → ran 𝐴 ∈ HF )
8	1 2 7	3syl	⊢ ( 𝐴 ∈ HF → ran 𝐴 ∈ HF )