Definition df-hfstruct 46160

Description: Define the class of extensible structures whose components are all hereditarily finite. We will call these "HFStructs". Ideally, an HFStruct would itself be a hereditarily finite set, but this is not possible because the domain of a structure is, in the current formulation, a subset of ℕ. To get around this, we adjust the domain to be a subset of ω, obtaining the "converted form" (𝐹 ∘ (♯ ↾ ω)) of an HFStruct 𝐹. This is indeed hereditarily finite by hfstructhf 46166. Also, unlike general extensible structures, we do not allow ∅ to be a member of an HFStruct. This restriction gives us the property that two HFStructs are equal if and only if their converted forms are equal (hfstructcan 46167). (Contributed by Eric Schmidt, 29-Sep-2026.)

Assertion

Ref	Expression
df-hfstruct	⊢ HFStruct = (dom Struct ∩ 𝒫 (V × HF ))

Detailed syntax breakdown of Definition df-hfstruct

Step	Hyp	Ref	Expression
1		chfstruct 46159	. 2 class HFStruct
2		cstr 17333	. . . 4 class Struct
3	2	cdm 5651	. . 3 class dom Struct
4		cvv 3450	. . . . 5 class V
5		chf 9911	. . . . 5 class HF
6	4, 5	cxp 5649	. . . 4 class (V × HF )
7	6	cpw 4556	. . 3 class 𝒫 (V × HF )
8	3, 7	cin 4088	. 2 class (dom Struct ∩ 𝒫 (V × HF ))
9	1, 8	wceq 1569	1 wff HFStruct = (dom Struct ∩ 𝒫 (V × HF ))

This definition is used by:  hfstructstruct  46161  hfstructfun  46162  rnhfstructsshf  46163  ishfstruct  46164