Metamath Proof Explorer

Theorem hashomiso

Description: The # function yields an order isomorphism between _om and NN0 . (Contributed by Eric Schmidt, 7-Jul-2026)

Ref Expression
Assertion hashomiso 
|- ( # |` _om ) Isom _E , < ( _om , NN0 )

Proof

Step Hyp Ref Expression
1 hashomf1o 
 |-  ( # |` _om ) : _om -1-1-onto-> NN0
2 epel 
 |-  ( x _E y <-> x e. y )
3 hashnnltb 
 |-  ( ( x e. _om /\ y e. _om ) -> ( x e. y <-> ( # ` x ) < ( # ` y ) ) )
4 2 3 bitrid 
 |-  ( ( x e. _om /\ y e. _om ) -> ( x _E y <-> ( # ` x ) < ( # ` y ) ) )
5 fvres 
 |-  ( x e. _om -> ( ( # |` _om ) ` x ) = ( # ` x ) )
6 fvres 
 |-  ( y e. _om -> ( ( # |` _om ) ` y ) = ( # ` y ) )
7 5 6 breqan12d 
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( ( # |` _om ) ` x ) < ( ( # |` _om ) ` y ) <-> ( # ` x ) < ( # ` y ) ) )
8 4 7 bitr4d 
 |-  ( ( x e. _om /\ y e. _om ) -> ( x _E y <-> ( ( # |` _om ) ` x ) < ( ( # |` _om ) ` y ) ) )
9 8 rgen2 
 |-  A. x e. _om A. y e. _om ( x _E y <-> ( ( # |` _om ) ` x ) < ( ( # |` _om ) ` y ) )
10 df-isom 
 |-  ( ( # |` _om ) Isom _E , < ( _om , NN0 ) <-> ( ( # |` _om ) : _om -1-1-onto-> NN0 /\ A. x e. _om A. y e. _om ( x _E y <-> ( ( # |` _om ) ` x ) < ( ( # |` _om ) ` y ) ) ) )
11 1 9 10 mpbir2an 
 |-  ( # |` _om ) Isom _E , < ( _om , NN0 )