Theorem rnhfstructhf

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

	Ref	Expression
Assertion	rnhfstructhf	Could not format assertion : No typesetting found for |- ( F e. HFStruct -> ran F e. HF ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		hfstructstruct	Could not format ( F e. HFStruct -> E. x F Struct x ) : No typesetting found for |- ( F e. HFStruct -> E. x F Struct x ) with typecode |-
2		rnstructfi	$$⊢F\mathrm{Struct}x\to \mathrm{ran}F\in \mathrm{Fin}$$
3	2	exlimiv	$$⊢\exists xF\mathrm{Struct}x\to \mathrm{ran}F\in \mathrm{Fin}$$
4	1 3	syl	Could not format ( F e. HFStruct -> ran F e. Fin ) : No typesetting found for |- ( F e. HFStruct -> ran F e. Fin ) with typecode |-
5		rnhfstructsshf	Could not format ( F e. HFStruct -> ran F C_ HF ) : No typesetting found for |- ( F e. HFStruct -> ran F C_ HF ) with typecode |-
6		elhf3	Could not format ( ran F e. HF <-> ( ran F e. Fin /\ ran F C_ HF ) ) : No typesetting found for |- ( ran F e. HF <-> ( ran F e. Fin /\ ran F C_ HF ) ) with typecode |-
7	4 5 6	sylanbrc	Could not format ( F e. HFStruct -> ran F e. HF ) : No typesetting found for |- ( F e. HFStruct -> ran F e. HF ) with typecode |-