### (Mathematical logic, model theory:)

The basic theorem:
Theorem. If a system of axioms has models of arbitrarily large finite sizes, then it has an infinite model.

Using the modern-day machinery of mathematical logic, this theorem is merely a somewhat trite consequence of the compactness theorem for first-order logic. But don't misjudge the people who discovered this amazing mix of logic and set theory!

Proof:
Let A be the system of axioms. Define the proposition Pk to be "there exist at least k different elements in the model". This can easily be written in first order logic as

x1., ..., ∃xk. x1≠x2 & ... & x1≠xk & ... & xk-1 ≠ xk,
and it works in any language since it uses nothing from the language. Let A' be the set A union {Pk : k >= 1}.

Any finite subset of A' has a model (since it contains some Pl with largest l, so any model for A with at least l elements is a model for that finite subset). By compactness, A' has a model!

But a model for A' must have infinitely many elements, as it has "at least k elements" for all k, and is also a model for A.

QED.

There are more powerful versions of the theorem around, that give you models of arbitrarily large infinite cardinalities.