Definition df-hfstruct 46023

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 46029. 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 46030). (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 46022	. 2 class HFStruct
2		cstr 17324	. . . 4 class Struct
3	2	cdm 5651	. . 3 class dom Struct
4		cvv 3451	. . . . 5 class V
5		chf 9904	. . . . 5 class HF
6	4, 5	cxp 5649	. . . 4 class (V × HF )
7	6	cpw 4557	. . 3 class 𝒫 (V × HF )
8	3, 7	cin 3898	. 2 class (dom Struct ∩ 𝒫 (V × HF ))
9	1, 8	wceq 1570	1 wff HFStruct = (dom Struct ∩ 𝒫 (V × HF ))

This definition is used by:  hfstructstruct  46024  hfstructfun  46025  rnhfstructsshf  46026  ishfstruct  46027