Theorem hfstructstruct

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

	Ref	Expression
Assertion	hfstructstruct	Could not format assertion : No typesetting found for |- ( F e. HFStruct -> E. x F Struct x ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elinel1	Could not format ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F e. dom Struct ) : No typesetting found for |- ( F e. ( dom Struct i^i ~P ( _V X. HF ) ) -> F e. dom Struct ) with typecode |-
2		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 |-
3	1 2	eleq2s	Could not format ( F e. HFStruct -> F e. dom Struct ) : No typesetting found for |- ( F e. HFStruct -> F e. dom Struct ) with typecode |-
4		eldmg	$$⊢F\in \mathrm{dom}\mathrm{Struct}\to \left(F\in \mathrm{dom}\mathrm{Struct}\leftrightarrow \exists xF\mathrm{Struct}x\right)$$
5	4	ibi	$$⊢F\in \mathrm{dom}\mathrm{Struct}\to \exists xF\mathrm{Struct}x$$
6	3 5	syl	Could not format ( F e. HFStruct -> E. x F Struct x ) : No typesetting found for |- ( F e. HFStruct -> E. x F Struct x ) with typecode |-