Definition df-lthfstruct 46231

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 46232 easier. (Contributed by Eric Schmidt, 24-Oct-2026.)

Assertion

Ref	Expression
df-lthfstruct	⊢ <HFStruct = {⟨𝑓, 𝑔⟩ ∣ ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑓) E ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑔)}

Distinct variable group:   𝑓,𝑔,ℎ

Detailed syntax breakdown of Definition df-lthfstruct

Step	Hyp	Ref	Expression
1		clthfstruct 46230	. 2 class <HFStruct
2		vf	. . . . . 6 setvar 𝑓
3	2	cv 1569	. . . . 5 class 𝑓
4		vh	. . . . . 6 setvar ℎ
5		chfstruct 46219	. . . . . 6 class HFStruct
6	4	cv 1569	. . . . . . . 8 class ℎ
7		chash 14498	. . . . . . . . 9 class ♯
8		com 7898	. . . . . . . . 9 class ω
9	7, 8	cres 5657	. . . . . . . 8 class (♯ ↾ ω)
10	6, 9	ccom 5659	. . . . . . 7 class (ℎ ∘ (♯ ↾ ω))
11		cackbij 46216	. . . . . . 7 class ackBij
12	10, 11	cfv 6555	. . . . . 6 class (ackBij‘(ℎ ∘ (♯ ↾ ω)))
13	4, 5, 12	cmpt 5189	. . . . 5 class (ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))
14	3, 13	cfv 6555	. . . 4 class ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑓)
15		vg	. . . . . 6 setvar 𝑔
16	15	cv 1569	. . . . 5 class 𝑔
17	16, 13	cfv 6555	. . . 4 class ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑔)
18		cep 5554	. . . 4 class E
19	14, 17, 18	wbr 5106	. . 3 wff ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑓) E ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑔)
20	19, 2, 15	copab 5170	. 2 class {⟨𝑓, 𝑔⟩ ∣ ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑓) E ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑔)}
21	1, 20	wceq 1570	1 wff <HFStruct = {⟨𝑓, 𝑔⟩ ∣ ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑓) E ((ℎ ∈ HFStruct ↦ (ackBij‘(ℎ ∘ (♯ ↾ ω))))‘𝑔)}

This definition is used by:  hfstructwe  46232