Theorem hfstructstruct

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

	Ref	Expression
Assertion	hfstructstruct	⊢ ( 𝐹 ∈ HFStruct → ∃ 𝑥 𝐹 Struct 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		elinel1	⊢ ( 𝐹 ∈ ( dom Struct ∩ 𝒫 ( V × HF ) ) → 𝐹 ∈ dom Struct )
2		df-hfstruct	⊢ HFStruct = ( dom Struct ∩ 𝒫 ( V × HF ) )
3	1 2	eleq2s	⊢ ( 𝐹 ∈ HFStruct → 𝐹 ∈ dom Struct )
4		eldmg	⊢ ( 𝐹 ∈ dom Struct → ( 𝐹 ∈ dom Struct ↔ ∃ 𝑥 𝐹 Struct 𝑥 ) )
5	4	ibi	⊢ ( 𝐹 ∈ dom Struct → ∃ 𝑥 𝐹 Struct 𝑥 )
6	3 5	syl	⊢ ( 𝐹 ∈ HFStruct → ∃ 𝑥 𝐹 Struct 𝑥 )