(As posted to sci.logic on 30-Oct-96, with annotations added.)
Theorem: The statement "There exists a non-empty set that is a subset
of its union" implies the Axiom of Infinity.
Proof: Let X be a nonempty set which is a subset of its union; the latter
property is equivalent to saying that for any y in X, there exists a z in X
such that y is in z.
Define by finite recursion a function F:omega-->(power X) such that
F_0 = 0 (See inf3lemb 4582.)
F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 4583.)
Note: ^ means intersect, < means \in ("element of").
(Finite recursion as typically done requires the existence of omega;
to avoid this we can just use transfinite recursion restricted to omega.
F is a class-term that is not necessarily a set at this point.)
Lemma 1. F_n subset F_n+1. (See inf3lem1 4585.)
Proof: By induction: F_0 subset F_1. If y < F_n+1, then y^X subset F_n,
so if F_n subset F_n+1, then y^X subset F_n+1, so y < F_n+2.
Lemma 2. F_n =/= X. (See inf3lem2 4586.)
Proof: By induction: F_0 =/= X because X is not empty. Assume F_n =/= X.
Then there is a y in X that is not in F_n. By definition of X, there is a
z in X that contains y. Suppose F_n+1 = X. Then z is in F_n+1, and z^X
contains y, so z^X is not a subset of F_n, contrary to the definition of
F_n+1.
Lemma 3. F_n =/= F_n+1. (See inf3lem3 4587.)
Proof: Using the identity y^X subset F_n <-> y^(X-F_n) = 0, we have
F_n+1 = {y<X | y^(X-F_n) = 0}. Let q = {y<X-F_n | y^(X-F_n) = 0}.
Then q subset F_n+1. Since X-F_n is not empty by Lemma 2 and q is the
set of \in-minimal elements of X-F_n, by Foundation q is not empty, so q
and therefore F_n+1 have an element not in F_n.
Lemma 4. F_n proper_subset F_n+1. (See inf3lem4 4588.)
Proof: Lemmas 1 and 3.
Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 4589.)
Proof: Fix m and use induction on n > m. Basis: F_m proper_subset F_m+1
by Lemma 4. Induction: Assume F_m proper_subset F_n. Then since F_n
proper_subset F_n+1, F_m proper_subset F_n+1 by transitivity of proper
subset.
By Lemma 5, F_m =/= F_n for m =/= n, so F is 1-1. (See inf3lem6 4590.)
Thus the inverse of F is a function with range omega and domain a subset
of power X, so omega exists by Replacement. (See inf3lem7 4591.)
Q.E.D.
|
Home
