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	⊢ <HFStruct = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑓 ) E ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑔 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clthfstruct	⊢ <HFStruct
1		vf	⊢ 𝑓
2		vg	⊢ 𝑔
3		vh	⊢ ℎ
4		chfstruct	⊢ HFStruct
5		cackbij	⊢ ackBij
6	3	cv	⊢ ℎ
7		chash	⊢ ♯
8		com	⊢ ω
9	7 8	cres	⊢ ( ♯ ↾ ω )
10	6 9	ccom	⊢ ( ℎ ∘ ( ♯ ↾ ω ) )
11	10 5	cfv	⊢ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) )
12	3 4 11	cmpt	⊢ ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) )
13	1	cv	⊢ 𝑓
14	13 12	cfv	⊢ ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑓 )
15		cep	⊢ E
16	2	cv	⊢ 𝑔
17	16 12	cfv	⊢ ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑔 )
18	14 17 15	wbr	⊢ ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑓 ) E ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑔 )
19	18 1 2	copab	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑓 ) E ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑔 ) }
20	0 19	wceq	⊢ <HFStruct = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑓 ) E ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑔 ) }