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	Could not format assertion : No typesetting found for |- HFStruct = ( dom Struct i^i ~P ( _V X. HF ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chfstruct	Could not format HFStruct : No typesetting found for class HFStruct with typecode class
1		cstr	$$class\mathrm{Struct}$$
2	1	cdm	$$class\mathrm{dom}\mathrm{Struct}$$
3		cvv	$$class\mathrm{V}$$
4		chf	Could not format HF : No typesetting found for class HF with typecode class
5	3 4	cxp	Could not format ( _V X. HF ) : No typesetting found for class ( _V X. HF ) with typecode class
6	5	cpw	Could not format ~P ( _V X. HF ) : No typesetting found for class ~P ( _V X. HF ) with typecode class
7	2 6	cin	Could not format ( dom Struct i^i ~P ( _V X. HF ) ) : No typesetting found for class ( dom Struct i^i ~P ( _V X. HF ) ) with typecode class
8	0 7	wceq	Could not format HFStruct = ( dom Struct i^i ~P ( _V X. HF ) ) : No typesetting found for wff HFStruct = ( dom Struct i^i ~P ( _V X. HF ) ) with typecode wff