Metamath Proof Explorer


Syntax definition wsmo

Description: Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals.

Ref Expression
Assertion wsmo wff Smo A