Definition df-hfstruct 46291

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 46297. 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 46298). The motivation for introducing this concept is to provide a general way of choosing a canonical representative of a class of finite structures. See df-finfld 46305 for an example of this idea. (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 46290	. 2 class HFStruct
2		cstr 17368	. . . 4 class Struct
3	2	cdm 5658	. . 3 class dom Struct
4		cvv 3454	. . . . 5 class V
5		chf 9941	. . . . 5 class HF
6	4, 5	cxp 5656	. . . 4 class (V × HF )
7	6	cpw 4560	. . 3 class 𝒫 (V × HF )
8	3, 7	cin 4092	. 2 class (dom Struct ∩ 𝒫 (V × HF ))
9	1, 8	wceq 1570	1 wff HFStruct = (dom Struct ∩ 𝒫 (V × HF ))

This definition is used by:  hfstructstruct  46292  hfstructfun  46293  rnhfstructsshf  46294  ishfstruct  46295