Michael Kleber wrote: <<
A set is finite if there exists no bijection of it onto one of its proper subsets.
Unfortunately, that's not true. Or rather, there are models of set theory in which this definition ("Dedekind-finite") is equivalent to the usual notion of "finite", but there are others in which it is not. The Axiom of Choice is more than enough to imply they are equivalent, but that seems like much more than you want to get into if you're looking for beautiful stand-alone theorems.
Actually, in suggesting the exercise [that boils down to] There is an injection i: X u {X} -> X <=> There is a surjection s: X -> X u {X}, it struck me that the => direction is simple enough, but the <= direction seems to require the Axiom of Choice. I.e., =>: ----------- Define a surjection S_i: X -> X u {X} via S_i(x) = i^(-1)(x), if x is in Im(i); else S_i(x) = X. But for <=: ------------- Define an injection I_s: X u {X} -> X via I_s(x) = some member of s^(-1)(x), if x is in s^(-1)(X); else I_s(x) = some member of s^(-1)(X). (I'm not sure how to get around the use of AC in <=.) --Dan