Theorem rnhfstructhf

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

	Ref	Expression
Assertion	rnhfstructhf	|- ( F e. HFStruct -> ran F e. HF )

Proof

Step	Hyp	Ref	Expression
1		hfstructstruct	|- ( F e. HFStruct -> E. x F Struct x )
2		rnstructfi	|- ( F Struct x -> ran F e. Fin )
3	2	exlimiv	|- ( E. x F Struct x -> ran F e. Fin )
4	1 3	syl	|- ( F e. HFStruct -> ran F e. Fin )
5		rnhfstructsshf	|- ( F e. HFStruct -> ran F C_ HF )
6		elhf3	|- ( ran F e. HF <-> ( ran F e. Fin /\ ran F C_ HF ) )
7	4 5 6	sylanbrc	|- ( F e. HFStruct -> ran F e. HF )