Theorem rnhfstructsshf

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

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

Proof

Step	Hyp	Ref	Expression
1		elinel2	⊢ ( 𝐹 ∈ ( dom Struct ∩ 𝒫 ( V × HF ) ) → 𝐹 ∈ 𝒫 ( V × HF ) )
2	1	elpwid	⊢ ( 𝐹 ∈ ( dom Struct ∩ 𝒫 ( V × HF ) ) → 𝐹 ⊆ ( V × HF ) )
3		df-hfstruct	⊢ HFStruct = ( dom Struct ∩ 𝒫 ( V × HF ) )
4	2 3	eleq2s	⊢ ( 𝐹 ∈ HFStruct → 𝐹 ⊆ ( V × HF ) )
5		rnss	⊢ ( 𝐹 ⊆ ( V × HF ) → ran 𝐹 ⊆ ran ( V × HF ) )
6	4 5	syl	⊢ ( 𝐹 ∈ HFStruct → ran 𝐹 ⊆ ran ( V × HF ) )
7		rnxpss	⊢ ran ( V × HF ) ⊆ HF
8	6 7	sstrdi	⊢ ( 𝐹 ∈ HFStruct → ran 𝐹 ⊆ HF )