Theorem hfstructstruct

Description: An HFStruct is an extensible structure. (Contributed by Eric Schmidt, 29-Sep-2026)

	Ref	Expression
Assertion	hfstructstruct	|- ( F e. HFStruct -> E. x F Struct x )

Proof

Step	Hyp	Ref	Expression
1		elinel1	|- ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F e. dom Struct )
2		df-hfstruct	|- HFStruct = ( dom Struct i^i ~P ( _V X. HF ) )
3	1 2	eleq2s	|- ( F e. HFStruct -> F e. dom Struct )
4		eldmg	|- ( F e. dom Struct -> ( F e. dom Struct <-> E. x F Struct x ) )
5	4	ibi	|- ( F e. dom Struct -> E. x F Struct x )
6	3 5	syl	|- ( F e. HFStruct -> E. x F Struct x )