Definition df-hfstruct

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 NN . To get around this, we adjust the domain to be a subset of _om , obtaining the "converted form" ` ( F o. ( # |`_om ) ) of an HFStruct F . This is indeed hereditarily finite by hfstructhf . 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 ). (Contributed by Eric Schmidt, 29-Sep-2026)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chfstruct	⊢ HFStruct
1		cstr	⊢ Struct
2	1	cdm	⊢ dom Struct
3		cvv	⊢ V
4		chf	⊢ HF
5	3 4	cxp	⊢ ( V × HF )
6	5	cpw	⊢ 𝒫 ( V × HF )
7	2 6	cin	⊢ ( dom Struct ∩ 𝒫 ( V × HF ) )
8	0 7	wceq	⊢ HFStruct = ( dom Struct ∩ 𝒫 ( V × HF ) )