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 i^i ~P ( _V X. 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 X. HF )
6	5	cpw	|- ~P ( _V X. HF )
7	2 6	cin	|- ( dom Struct i^i ~P ( _V X. HF ) )
8	0 7	wceq	|- HFStruct = ( dom Struct i^i ~P ( _V X. HF ) )