Metamath Proof Explorer

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 
|- . | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clthfstruct 
 |-
1 vf 
 |-  f
2 vg 
 |-  g
3 vh 
 |-  h
4 chfstruct 
 |-  HFStruct
5 cackbij 
 |-  ackBij
6 3 cv 
 |-  h
7 chash 
 |-  #
8 com 
 |-  _om
9 7 8 cres 
 |-  ( # |` _om )
10 6 9 ccom 
 |-  ( h o. ( # |` _om ) )
11 10 5 cfv 
 |-  ( ackBij ` ( h o. ( # |` _om ) ) )
12 3 4 11 cmpt 
 |-  ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) )
13 1 cv 
 |-  f
14 13 12 cfv 
 |-  ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f )
15 cep 
 |-  _E
16 2 cv 
 |-  g
17 16 12 cfv 
 |-  ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g )
18 14 17 15 wbr 
 |-  ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g )
19 18 1 2 copab 
 |-  { <. f , g >. | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) }
20 0 19 wceq 
 |-  . | ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` f ) _E ( ( h e. HFStruct |-> ( ackBij ` ( h o. ( # |` _om ) ) ) ) ` g ) }