Description: The codomain of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013)