Metamath Proof Explorer

Theorem rnhfstructsshf

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

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

Proof

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