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	Could not format assertion : No typesetting found for |-

Proof

Step	Hyp	Ref	Expression
1		hfstructhf	Could not format ( h e. HFStruct -> ( h o. ( # |` _om ) ) e. HF ) : No typesetting found for |- ( h e. HFStruct -> ( h o. ( # |` _om ) ) e. HF ) with typecode |-
2		ackbij3	Could not format ackBij : HF -1-1-onto-> _om : No typesetting found for |- ackBij : HF -1-1-onto-> _om with typecode |-
3		f1of	Could not format ( ackBij : HF -1-1-onto-> _om -> ackBij : HF --> _om ) : No typesetting found for |- ( ackBij : HF -1-1-onto-> _om -> ackBij : HF --> _om ) with typecode |-
4	2 3	ax-mp	Could not format ackBij : HF --> _om : No typesetting found for |- ackBij : HF --> _om with typecode |-
5	4	ffvelcdmi	Could not format ( ( h o. ( # |` _om ) ) e. HF -> ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om ) : No typesetting found for |- ( ( h o. ( # |` _om ) ) e. HF -> ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om ) with typecode |-
6	1 5	syl	Could not format ( h e. HFStruct -> ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om ) : No typesetting found for |- ( h e. HFStruct -> ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om ) with typecode |-
7	6	rgen	Could not format A. h e. HFStruct ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om : No typesetting found for |- A. h e. HFStruct ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om with typecode |-
8		hfstructhf	Could not format ( f e. HFStruct -> ( f o. ( # |` _om ) ) e. HF ) : No typesetting found for |- ( f e. HFStruct -> ( f o. ( # |` _om ) ) e. HF ) with typecode |-
9		f1of1	Could not format ( ackBij : HF -1-1-onto-> _om -> ackBij : HF -1-1-> _om ) : No typesetting found for |- ( ackBij : HF -1-1-onto-> _om -> ackBij : HF -1-1-> _om ) with typecode |-
10	2 9	ax-mp	Could not format ackBij : HF -1-1-> _om : No typesetting found for |- ackBij : HF -1-1-> _om with typecode |-
11		f1veqaeq	Could not format ( ( ackBij : HF -1-1-> _om /\ ( ( h o. ( # |` _om ) ) e. HF /\ ( f o. ( # |` _om ) ) e. HF ) ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) ) ) : No typesetting found for |- ( ( ackBij : HF -1-1-> _om /\ ( ( h o. ( # |` _om ) ) e. HF /\ ( f o. ( # |` _om ) ) e. HF ) ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) ) ) with typecode |-
12	10 11	mpan	Could not format ( ( ( h o. ( # |` _om ) ) e. HF /\ ( f o. ( # |` _om ) ) e. HF ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) ) ) : No typesetting found for |- ( ( ( h o. ( # |` _om ) ) e. HF /\ ( f o. ( # |` _om ) ) e. HF ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) ) ) with typecode |-
13	1 8 12	syl2an	Could not format ( ( h e. HFStruct /\ f e. HFStruct ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) ) ) : No typesetting found for |- ( ( h e. HFStruct /\ f e. HFStruct ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) ) ) with typecode |-
14		hfstructcan	Could not format ( ( h e. HFStruct /\ f e. HFStruct ) -> ( ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) <-> h = f ) ) : No typesetting found for |- ( ( h e. HFStruct /\ f e. HFStruct ) -> ( ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) <-> h = f ) ) with typecode |-
15	13 14	sylibd	Could not format ( ( h e. HFStruct /\ f e. HFStruct ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> h = f ) ) : No typesetting found for |- ( ( h e. HFStruct /\ f e. HFStruct ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> h = f ) ) with typecode |-
16	15	rgen2	Could not format A. h e. HFStruct A. f e. HFStruct ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> h = f ) : No typesetting found for |- A. h e. HFStruct A. f e. HFStruct ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> h = f ) with typecode |-
17		eqid	Could not format ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) = ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : No typesetting found for |- ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) = ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) with typecode |-
18		coeq1	$$⊢h=f\to h\circ \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)=f\circ \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)$$
19	18	fveq2d	Could not format ( h = f -> ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) ) : No typesetting found for |- ( h = f -> ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) ) with typecode |-
20	17 19	f1mpt	Could not format ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : HFStruct -1-1-> _om <-> ( A. h e. HFStruct ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om /\ A. h e. HFStruct A. f e. HFStruct ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> h = f ) ) ) : No typesetting found for |- ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : HFStruct -1-1-> _om <-> ( A. h e. HFStruct ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om /\ A. h e. HFStruct A. f e. HFStruct ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> h = f ) ) ) with typecode |-
21	7 16 20	mpbir2an	Could not format ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : HFStruct -1-1-> _om : No typesetting found for |- ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : HFStruct -1-1-> _om with typecode |-
22		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
23		ordwe	$$⊢\mathrm{Ord}\mathrm{\omega }\to \mathrm{E}\mathrm{We}\mathrm{\omega }$$
24	22 23	ax-mp	$$⊢\mathrm{E}\mathrm{We}\mathrm{\omega }$$
25		df-lthfstruct	Could not format . | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) } : No typesetting found for |- . | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) } with typecode |-
26	25	f1we	Could not format ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : HFStruct -1-1-> _om -> ( _E We _om -> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : HFStruct -1-1-> _om -> ( _E We _om ->
27	21 24 26	mp2	Could not format