Theorem hfstructwe

Description: The relation is a well ordering of the class of HFStructs. (Contributed by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Assertion	hfstructwe	⊢ <HFStruct We HFStruct

Proof

Step	Hyp	Ref	Expression
1		hfstructhf	⊢ ( ℎ ∈ HFStruct → ( ℎ ∘ ( ♯ ↾ ω ) ) ∈ HF )
2		ackbij3	⊢ ackBij : HF ⟶1-1onto ω
3		f1of	⊢ ( ackBij : HF ⟶1-1onto ω → ackBij : HF ⟶ ω )
4	2 3	ax-mp	⊢ ackBij : HF ⟶ ω
5	4	ffvelcdmi	⊢ ( ( ℎ ∘ ( ♯ ↾ ω ) ) ∈ HF → ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ∈ ω )
6	1 5	syl	⊢ ( ℎ ∈ HFStruct → ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ∈ ω )
7	6	rgen	⊢ ∀ ℎ ∈ HFStruct ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ∈ ω
8		hfstructhf	⊢ ( 𝑓 ∈ HFStruct → ( 𝑓 ∘ ( ♯ ↾ ω ) ) ∈ HF )
9		f1of1	⊢ ( ackBij : HF ⟶1-1onto ω → ackBij : HF ⟶1-1 ω )
10	2 9	ax-mp	⊢ ackBij : HF ⟶1-1 ω
11		f1veqaeq	⊢ ( ( ackBij : HF ⟶1-1 ω ∧ ( ( ℎ ∘ ( ♯ ↾ ω ) ) ∈ HF ∧ ( 𝑓 ∘ ( ♯ ↾ ω ) ) ∈ HF ) ) → ( ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) = ( ackBij ‘ ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) → ( ℎ ∘ ( ♯ ↾ ω ) ) = ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) )
12	10 11	mpan	⊢ ( ( ( ℎ ∘ ( ♯ ↾ ω ) ) ∈ HF ∧ ( 𝑓 ∘ ( ♯ ↾ ω ) ) ∈ HF ) → ( ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) = ( ackBij ‘ ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) → ( ℎ ∘ ( ♯ ↾ ω ) ) = ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) )
13	1 8 12	syl2an	⊢ ( ( ℎ ∈ HFStruct ∧ 𝑓 ∈ HFStruct ) → ( ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) = ( ackBij ‘ ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) → ( ℎ ∘ ( ♯ ↾ ω ) ) = ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) )
14		hfstructcan	⊢ ( ( ℎ ∈ HFStruct ∧ 𝑓 ∈ HFStruct ) → ( ( ℎ ∘ ( ♯ ↾ ω ) ) = ( 𝑓 ∘ ( ♯ ↾ ω ) ) ↔ ℎ = 𝑓 ) )
15	13 14	sylibd	⊢ ( ( ℎ ∈ HFStruct ∧ 𝑓 ∈ HFStruct ) → ( ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) = ( ackBij ‘ ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) → ℎ = 𝑓 ) )
16	15	rgen2	⊢ ∀ ℎ ∈ HFStruct ∀ 𝑓 ∈ HFStruct ( ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) = ( ackBij ‘ ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) → ℎ = 𝑓 )
17		eqid	⊢ ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) = ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) )
18		coeq1	⊢ ( ℎ = 𝑓 → ( ℎ ∘ ( ♯ ↾ ω ) ) = ( 𝑓 ∘ ( ♯ ↾ ω ) ) )
19	18	fveq2d	⊢ ( ℎ = 𝑓 → ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) = ( ackBij ‘ ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) )
20	17 19	f1mpt	⊢ ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) : HFStruct ⟶1-1 ω ↔ ( ∀ ℎ ∈ HFStruct ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ∈ ω ∧ ∀ ℎ ∈ HFStruct ∀ 𝑓 ∈ HFStruct ( ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) = ( ackBij ‘ ( 𝑓 ∘ ( ♯ ↾ ω ) ) ) → ℎ = 𝑓 ) ) )
21	7 16 20	mpbir2an	⊢ ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) : HFStruct ⟶1-1 ω
22		ordom	⊢ Ord ω
23		ordwe	⊢ ( Ord ω → E We ω )
24	22 23	ax-mp	⊢ E We ω
25		df-lthfstruct	⊢ <HFStruct = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑓 ) E ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) ‘ 𝑔 ) }
26	25	f1we	⊢ ( ( ℎ ∈ HFStruct ↦ ( ackBij ‘ ( ℎ ∘ ( ♯ ↾ ω ) ) ) ) : HFStruct ⟶1-1 ω → ( E We ω → <HFStruct We HFStruct ) )
27	21 24 26	mp2	⊢ <HFStruct We HFStruct