Theorem rnhfstructsshf

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

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

Proof

Step	Hyp	Ref	Expression
1		elinel2	Could not format ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F e. ~P ( _V X. HF ) ) : No typesetting found for |- ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F e. ~P ( _V X. HF ) ) with typecode |-
2	1	elpwid	Could not format ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F C_ ( _V X. HF ) ) : No typesetting found for |- ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F C_ ( _V X. HF ) ) with typecode |-
3		df-hfstruct	Could not format HFStruct = ( dom Struct i^i ~P ( _V X. HF ) ) : No typesetting found for |- HFStruct = ( dom Struct i^i ~P ( _V X. HF ) ) with typecode |-
4	2 3	eleq2s	Could not format ( F e. HFStruct -> F C_ ( _V X. HF ) ) : No typesetting found for |- ( F e. HFStruct -> F C_ ( _V X. HF ) ) with typecode |-
5		rnss	Could not format ( F C_ ( _V X. HF ) -> ran F C_ ran ( _V X. HF ) ) : No typesetting found for |- ( F C_ ( _V X. HF ) -> ran F C_ ran ( _V X. HF ) ) with typecode |-
6	4 5	syl	Could not format ( F e. HFStruct -> ran F C_ ran ( _V X. HF ) ) : No typesetting found for |- ( F e. HFStruct -> ran F C_ ran ( _V X. HF ) ) with typecode |-
7		rnxpss	Could not format ran ( _V X. HF ) C_ HF : No typesetting found for |- ran ( _V X. HF ) C_ HF with typecode |-
8	6 7	sstrdi	Could not format ( F e. HFStruct -> ran F C_ HF ) : No typesetting found for |- ( F e. HFStruct -> ran F C_ HF ) with typecode |-