Description: The value of the cardinal number function with an ordinal number as its argument. Unlike cardval , this theorem does not require the Axiom of Choice. (Contributed by NM, 24-Nov-2003) (Revised by Mario Carneiro, 13-Sep-2013)