Theorem rnhfstructhf

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

	Ref	Expression
Assertion	rnhfstructhf	⊢ ( 𝐹 ∈ HFStruct → ran 𝐹 ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		hfstructstruct	⊢ ( 𝐹 ∈ HFStruct → ∃ 𝑥 𝐹 Struct 𝑥 )
2		rnstructfi	⊢ ( 𝐹 Struct 𝑥 → ran 𝐹 ∈ Fin )
3	2	exlimiv	⊢ ( ∃ 𝑥 𝐹 Struct 𝑥 → ran 𝐹 ∈ Fin )
4	1 3	syl	⊢ ( 𝐹 ∈ HFStruct → ran 𝐹 ∈ Fin )
5		rnhfstructsshf	⊢ ( 𝐹 ∈ HFStruct → ran 𝐹 ⊆ HF )
6		elhf3	⊢ ( ran 𝐹 ∈ HF ↔ ( ran 𝐹 ∈ Fin ∧ ran 𝐹 ⊆ HF ) )
7	4 5 6	sylanbrc	⊢ ( 𝐹 ∈ HFStruct → ran 𝐹 ∈ HF )