Description: Axiom of Infinity. An
axiom of Zermelo-Fraenkel set theory. This axiom
is the gateway to "Cantor's paradise" (an expression coined by
Hilbert). It asserts that given a starting set , an infinite set
built from it exists. Although our version is
apparently not
given in the literature, it is similar to, but slightly shorter than,
the Axiom of Infinity in [FreydScedrov] p. 283 (see inf18060
and
inf28061). More standard versions, which essentially
state that there
exists a set containing all the natural numbers, are shown as zfinf28080
and omex8081 and are based on the (nontrivial) proof of inf38073.
This
version has the advantage that when expanded to primitives, it has fewer
symbols than the standard version ax-inf28079. Theorem inf08059
shows the
reverse derivation of our axiom from a standard one. Theorem inf58083
shows a very short way to state this axiom.

The standard version of Infinity ax-inf28079 requires this axiom along
with Regularity ax-reg8039 for its derivation (as theorem axinf28078
below). In order to more easily identify the normal uses of Regularity,
we will usually reference ax-inf28079 instead of this one. The derivation
of this axiom from ax-inf28079 is shown by theorem axinf8082.

Proofs should normally use the standard version ax-inf28079 instead of
this axiom. (New usage is discouraged.) (Contributed by NM,
16-Aug-1993.)