Definition df-lthfstruct

Description: Define a well ordering on HFStructs. The exact definition is not important. Any explicit definition of a well ordering would do. The definition we have chosen makes proving hfstructwe easier. (Contributed by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Assertion	df-lthfstruct	Could not format assertion : No typesetting found for |- . | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clthfstruct	Could not format
1		vf	$$setvarf$$
2		vg	$$setvarg$$
3		vh	$$setvarh$$
4		chfstruct	Could not format HFStruct : No typesetting found for class HFStruct with typecode class
5		cackbij	Could not format ackBij : No typesetting found for class ackBij with typecode class
6	3	cv	$$setvarh$$
7		chash	$$class\left|.\right|$$
8		com	$$class\mathrm{\omega }$$
9	7 8	cres	$$class\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)$$
10	6 9	ccom	$$class\left(h\circ \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\right)$$
11	10 5	cfv	Could not format ( ackBij ` ( h o. ( # |` _om ) ) ) : No typesetting found for class ( ackBij ` ( h o. ( # |` _om ) ) ) with typecode class
12	3 4 11	cmpt	Could not format ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : No typesetting found for class ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) with typecode class
13	1	cv	$$setvarf$$
14	13 12	cfv	Could not format ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) : No typesetting found for class ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) with typecode class
15		cep	$$class\mathrm{E}$$
16	2	cv	$$setvarg$$
17	16 12	cfv	Could not format ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) : No typesetting found for class ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) with typecode class
18	14 17 15	wbr	Could not format ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) : No typesetting found for wff ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) with typecode wff
19	18 1 2	copab	Could not format { <. f , g >. | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) } : No typesetting found for class { <. f , g >. | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) } with typecode class
20	0 19	wceq	Could not format . | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) } : No typesetting found for wff . | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) } with typecode wff