Metamath Proof Explorer


Syntax definition ciomnn

Description: Syntax for the canonical bijection from (om u. { om } ) onto ( NN0 u. { pinfty } ) .

Ref Expression
Assertion ciomnn class i ω↪ℕ