Metamath Proof Explorer

Theorem hashomf1o

Description: The # function yields a bijection from _om to NN0 . (Contributed by Eric Schmidt, 7-Jul-2026)

Ref Expression
Assertion hashomf1o 
|- ( # |` _om ) : _om -1-1-onto-> NN0

Proof

Step Hyp Ref Expression
1 hashgval2 
 |-  ( # |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2 1 hashgf1o 
 |-  ( # |` _om ) : _om -1-1-onto-> NN0