Metamath Proof Explorer

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 
|-

Proof

Step Hyp Ref Expression
1 hfstructhf 
 |-  ( h e. HFStruct -> ( h o. ( # |` _om ) ) e. HF )
2 ackbij3 
 |-  ackBij : HF -1-1-onto-> _om
3 f1of 
 |-  ( ackBij : HF -1-1-onto-> _om -> ackBij : HF --> _om )
4 2 3 ax-mp 
 |-  ackBij : HF --> _om
5 4 ffvelcdmi 
 |-  ( ( h o. ( # |` _om ) ) e. HF -> ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om )
6 1 5 syl 
 |-  ( h e. HFStruct -> ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om )
7 6 rgen 
 |-  A. h e. HFStruct ( ackBij ` ( h o. ( # |` _om ) ) ) e. _om
8 hfstructhf 
 |-  ( f e. HFStruct -> ( f o. ( # |` _om ) ) e. HF )
9 f1of1 
 |-  ( ackBij : HF -1-1-onto-> _om -> ackBij : HF -1-1-> _om )
10 2 9 ax-mp 
 |-  ackBij : HF -1-1-> _om
11 f1veqaeq 
 |-  ( ( 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 ) ) ) )
12 10 11 mpan 
 |-  ( ( ( h o. ( # |` _om ) ) e. HF /\ ( f o. ( # |` _om ) ) e. HF ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) ) )
13 1 8 12 syl2an 
 |-  ( ( h e. HFStruct /\ f e. HFStruct ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) ) )
14 hfstructcan 
 |-  ( ( h e. HFStruct /\ f e. HFStruct ) -> ( ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) <-> h = f ) )
15 13 14 sylibd 
 |-  ( ( h e. HFStruct /\ f e. HFStruct ) -> ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> h = f ) )
16 15 rgen2 
 |-  A. h e. HFStruct A. f e. HFStruct ( ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) -> h = f )
17 eqid 
 |-  ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) = ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) )
18 coeq1 
 |-  ( h = f -> ( h o. ( # |` _om ) ) = ( f o. ( # |` _om ) ) )
19 18 fveq2d 
 |-  ( h = f -> ( ackBij ` ( h o. ( # |` _om ) ) ) = ( ackBij ` ( f o. ( # |` _om ) ) ) )
20 17 19 f1mpt 
 |-  ( ( 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 ) ) )
21 7 16 20 mpbir2an 
 |-  ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : HFStruct -1-1-> _om
22 ordom 
 |-  Ord _om
23 ordwe 
 |-  ( Ord _om -> _E We _om )
24 22 23 ax-mp 
 |-  _E We _om
25 df-lthfstruct 
 |-  . | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) }
26 25 f1we 
 |-  ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) : HFStruct -1-1-> _om -> ( _E We _om ->
27 21 24 26 mp2 
 |-