Description: The Hartogs number of a set is greater than all ordinals which inject into it. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 15-May-2015)