HomeHome Metamath Proof Explorer < Previous   Next >
Browser slow? Try the
Unicode version.
Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10690

Color key:    Metamath Proof Explorer  Metamath Proof Explorer (1-8762)   Hilbert Space Explorer  Hilbert Space Explorer (8763-10690)  

Statement List for Metamath Proof Explorer - 4601-4700 - Page 47 of 107
TypeLabelDescription
Statement
 
Theoreminf2 4601 Variation of Axiom of Infinity. There exists a non-empty set that is a subset of its union (using axinf 4616 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283.
|- E.x(y e. x /\ A.y(y e. x -> E.z(y e. z /\ z e. x)))   =>   |- E.x(x =/= (/) /\ x (_ U.x)
 
Theoreminf3lema 4602 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description.
 
Theoreminf3lemb 4603 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description.
 
Theoreminf3lemc 4604 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description.
 
Theoreminf3lemd 4605 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description.
 
Theoreminf3lem1 4606 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description.
 
Theoreminf3lem2 4607 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description.
 
Theoreminf3lem3 4608 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 4589.
 
Theoreminf3lem4 4609 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description.
 
Theoreminf3lem5 4610 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description.
 
Theoreminf3lem6 4611 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description.
 
Theoreminf3lem7 4612 Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4613 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of funrnex 3616.
 
Theoreminf3 4613 Our Axiom of Infinity ax-inf 4615 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 4601, and the conclusion is the version of the Axiom of Infinity shown as Axiom 7 in [TakeutiZaring] p. 43. (Other standard versions are proved later as axinf2 4617 and zfinf 4619.) The main proof is provided by inf3lema 4602 through inf3lem7 4612, and this final piece eliminates the auxiliary hypothesis of inf3lem7 4612. This proof is due to Ian Sutherland, Richard Heck, and Norman Megill and was posted on Usenet as shown below. Although the result is not new, the authors were unable to find a published proof. 

(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 4603.)
  F_n+1 = {y<X | y^X subset F_n}  (See inf3lemc 4604.)
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 4606.)
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 4607.)
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 4608.)
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 4609.)
Proof:  Lemmas 1 and 3.

Lemma 5.  F_m proper_subset F_n, m < n.  (See inf3lem5 4610.)
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 4611.)
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 4612.)
Q.E.D.
|- E.x(x =/= (/) /\ x (_ U.x)   =>   |- om e. V
 
Theoreminfeq5 4614 The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (shown on the right-hand side in the form of omex 4620.) The left-hand side provides us with a very short way to express of the Axiom of Infinity using only elementary symbols. This proof of equivalence does not depend on the Axiom of Infinity.
|- (E.x x (. U.x <-> om e. V)
 
ZF Set Theory - add the Axiom of Infinity
 
Introduce the Axiom of Infinity
 
Axiomax-inf 4615 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 x, an infinite set y 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 inf1 4600 and inf2 4601). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf 4619 and omex 4620 and are based on the (nontrivial) proof of inf3 4613. Our version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 4618. Theorem inf0 4599 shows the reverse derivation of our axiom from a standard one. Theorem inf5 4621 shows a very short way to state this axiom.

An interesting property of our version is that, unlike the standard version, it does not assert the independent existence of any set; it needs a starting set x. Since none of our other ZFC axioms assert the independent existence of any set, we would need to add an axiom of existence such as Axiom 0 of [Kunen] p. 10 if we were to use a "free logic" predicate calculus that (unlike ours) does not assert (as we do with ax-4 971 and ax-9 963) that at least one thing exists.

The standard version of Infinity ax-inf2 4618 requires this axiom along with Regularity ax-reg 4586 for its derivation (as theorem axinf2 4617 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 4618 instead of this one.

|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
 
Theoremaxinf 4616 Axiom of Infinity expressed with fewest number of different variables.
|- E.x(y e. x /\ A.y(y e. x -> E.z(y e. z /\ z e. x)))
 
Theoremaxinf2 4617 A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 4615 and Regularity ax-reg 4586.

This theorem should not be referenced in any proof. Instead, use ax-inf2 4618 below so that the ordinary uses of Regularity can be more easily identified.

|- E.x(E.y(y e. x /\ A.z -. z e. y) /\ A.y(y e. x -> E.z(z e. x /\ A.w(w e. z <-> (w e. y \/ w = y)))))
 
Axiomax-inf2 4618 A standard version of Axiom of Infinity of ZF set theory. In English, it says: there exists a set that contains the empty set and the successors of all of its members. Theorem zfinf 4619 shows it converted to abbreviations. This axiom was derived as theorem axinf2 4617 above, using our version of Infinity ax-inf 4615 and the Axiom of Regularity ax-reg 4586. We will reference ax-inf2 4618 instead of axinf2 4617 so that the ordinary uses of Regularity can be more easily identified.
|- E.x(E.y(y e. x /\ A.z -. z e. y) /\ A.y(y e. x -> E.z(z e. x /\ A.w(w e. z <-> (w e. y \/ w = y)))))
 
Theoremzfinf 4619 A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 4618 for the unabbreviated version.)
|- E.x((/) e. x /\ A.y e. x suc y e. x)
 
Existence of omega (the set of natural numbers)
 
Theoremomex 4620 The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 4599.

A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial -. om e. V; this would lead to om = On (the proper class of ordinals) by omon 3143 and onprc 2989. The finitist could still develop natural number, integer, and rational number arithmetic but would be denied the real numbers (as well as much of the rest of mathematics). In deference to the finitist, much of our development is done, when possible, without invoking the Axiom of Infinity; an example is Peano's axioms peano1 3149 through peano5 3153 (which many textbooks prove more easily assuming Infinity).

|- om e. V
 
Theoreminf5 4621 The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see theorem infeq5 4614). This provides us with a very compact way to express of the Axiom of Infinity using only elementary symbols.
|- E.x x (. U.x
 
Theoremomelon 4622 Omega is an ordinal number.
|- om e. On
 
Theoremdfom3 4623 The class of natural numbers omega can be defined as the smallest "inductive set," which is valid provided we assume the Axiom of Infinity. Definition 6.3 of [Eisenberg] p. 82.
|- om = |^|{x | ((/) e. x /\ A.y e. x suc y e. x)}
 
Theoremelom3 4624 A simplification of elom 3134 assuming the Axiom of Infinity.
|- (A e. om <-> A.x(Lim x -> A e. x))
 
Theoremdfom4 4625 A simplification of df-om 3132 assuming the Axiom of Infinity.
|- om = {x | A.y(Lim y -> x e. y)}
 
Theoremoancom 4626 Ordinal addition is not commutative. This theorem shows a counterexample. Remark in [TakeutiZaring] p. 60.
|- (1o +o om) =/= (om +o 1o)
 
Theoremisfinite 4627 A set is strictly dominated by the class of natural numbers iff it is finite. Theorem 42 of [Suppes] p. 151. This theorem provides two equivalent ways to express "A is finite." The Axiom of Infinity is used for the reverse implication.
|- (A ~< om <-> E.x e. om A ~~ x)
 
Theoremnnsdom 4628 A natural number is strictly dominated by the set of natural numbers.
|- (A e. om -> A ~< om)
 
Theoremomenps 4629 Omega is equinumerous to a proper subset of itself. Example 13.2(4) of [Eisenberg] p. 216.
|- om ~~ (om \ {(/)})
 
Theoremomensuc 4630 The set of natural numbers is equinumerous to its successor.
|- om ~~ suc om
 
Theoreminfensuc 4631 Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88.
|- ((A e. On /\ om (_ A) -> A ~~ suc A)
 
Theoremunbnnt 4632 Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 4540 eliminates its hypothesis by assuming the Axiom of Infinity.
|- ((A (_ om /\ A.x e. om E.y e. A x e. y) -> A ~~ om)
 
Theoremnoinfep 4633 Using the Axiom of Regularity in the form zfregfr 4594, show that there are no infinite descending e. -chains. Proposition 7.34 of [TakeutiZaring] p. 44.
|- (F Fn om -> E.x e. om -. (F` suc x) e. (F` x))
 
Rank
 
Syntaxcr1 4634 Extend class definition to include the cumulative hierarchy of sets function.
class R1
 
Syntaxcrnk 4635 Extend class definition to include rank function.
class rank
 
Definitiondf-r1 4636 Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation (R1). Starting with the empty set, this function builds up layers of sets where the next layer is the power set of the previous layer (and the union of previous layers when the argument is a limit ordinal). Using the Axiom of Regularity, we can show that any set whatsoever belongs to one of the layers of this hierarchy (see tz9.13 4656). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 4644, r1suc 4645, and r1lim 4646. Theorem r1val1 4651 shows a recursive definition that works for all values, and theorems r1val2 4671 and r1val3 4672 show the value expressed in terms of rank. Other notations for this function are R with the argument as a subscript (Equation 3.1 of [BellMachover] p. 477), V with a a subscript (Definition of [Enderton] p. 202), M with a subscript (Definition 15.19 of [Monk1] p. 113), the capital Greek letter psi (Definition of [Mendelson] p. 281), and bold-face R (Definition 2.1 of [Kunen] p. 95).
|- R1 = rec({<.x, y>. | y = P~x}, (/))
 
Definitiondf-rank 4637 Define the rank function. See rankval 4661, rankval2 4663, rankval3 4674, or rankval4 4695 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function R1: given a set, it returns an ordinal number telling us the smallest layer of the hierarchy to which the set belongs. Based on Definition 9.14 of [TakeutiZaring] p. 79. Theorem rankid 4665 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 4670.
|- rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}
 
Theoremtrcl 4638 For any set A, show the properties of its transitive closure C. Similar to Theorem 9.1 of [TakeutiZaring] p. 73 except that we show an explicit expression for the transitive closure rather than just its existence. See tz9.1 4639 for an abbreviated version showing existence.
|- A e. V   &   |- F = (rec({<.z, w>. | w = (z u. U.z)}, A) |` om)   &   |- C = U_y e. om (F` y)   =>   |- (A (_ C /\ Tr C /\ A.x((A (_ x /\ Tr x) -> C (_ x))
 
Theoremtz9.1 4639 Every set has a transitive closure (smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 4638 for an explicit expression for the transitive closure.
|- A e. V   =>   |- E.x(A (_ x /\ Tr x /\ A.y((A (_ y /\ Tr y) -> x (_ y))
 
Theoremzfregs 4640 The strong form of the Axiom of Regularity, which does not require that A be a set. Axiom 6' of [TakeutiZaring] p. 21. The proof makes use of a special case of Proposition 9.4 of [TakeutiZaring] p. 75.
|- (A =/= (/) -> E.x e. A (x i^i A) = (/))
 
Theoremsetind 4641 Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21.
|- (A.x(x (_ A -> x e. A) -> A = V)
 
Theoremsetind2 4642 Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996).
|- (P~A (_ A -> A = V)
 
Theoremr1fnon 4643 The cumulative hierarchy of sets function is a function on the class of ordinal numbers.
|- R1 Fn On
 
Theoremr10 4644 Value of the cumulative hierarchy of sets function at (/). Part of Definition 9.9 of [TakeutiZaring] p. 76.
|- (R1` (/)) = (/)
 
Theoremr1suc 4645 Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76.
|- (A e. On -> (R1` suc A) = P~(R1` A))
 
Theoremr1lim 4646 Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76.
|- ((A e. B /\ Lim A) -> (R1` A) = U_x e. A (R1` x))
 
Theoremr1tr 4647 The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202.
|- Tr (R1` A)
 
Theoremr1ord 4648 Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77.
|- (B e. On -> (A e. B -> (R1` A) e. (R1` B)))
 
Theoremr1ord2 4649 Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77.
|- (B e. On -> (A e. B -> (R1` A) (_ (R1` B)))
 
Theoremr1ord3 4650 Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478.
|- ((A e. On /\ B e. On) -> (A (_ B -> (R1` A) (_ (R1` B)))
 
Theoremr1val1 4651 The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202.
|- (A e. On -> (R1` A) = U_x e. A P~(R1` x))
 
Theoremtz9.12lem1 4652 Lemma for tz9.12 4655.
 
Theoremtz9.12lem2 4653 Lemma for tz9.12 4655.
 
Theoremtz9.12lem3 4654 Lemma for tz9.12 4655.
 
Theoremtz9.12 4655 A set is well-founded if all of its elements are well-founded. Proposition 9.12 of [TakeutiZaring] p. 78. The main proof consists of tz9.12lem1 4652 through tz9.12lem3 4654.
|- A e. V   =>   |- (A.x e. A E.y e. On x e. (R1` y) -> E.y e. On A e. (R1` y))
 
Theoremtz9.13 4656 Every set is well-founded, assuming the Axiom of Regularity. In other words, every set belongs to a layer of the cumulative hierarchy of sets. Proposition 9.13 of [TakeutiZaring] p. 78.
|- A e. V   =>   |- E.x e. On A e. (R1` x)
 
Theoremtz9.13g 4657 Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 4656 expresses the class existence requirement as an antecedent.
|- (A e. B -> E.x e. On A e. (R1` x))
 
Theoremrankwflem 4658 Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 4657 is useful in proofs of theorems about the rank function.
|- (A e. B -> E.x e. On A e. (R1` suc x))
 
Theoremjech9.3 4659 Every set belongs to some value of the cumulative hierarchy of sets function R1, i.e. the indexed union of all values of R1 is the universe. Lemma 9.3 of [Jech] p. 71.
|- U_x e. On (R1` x) = V
 
Theoremunir1 4660 The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of [Mendelson] p. 281.
|- U.(R1"On) = V
 
Theoremrankval 4661 Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition).
|- A e. V   =>   |- (rank` A) = |^|{x e. On | A e. (R1` suc x)}
 
Theoremrankvalg 4662 Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 4661 expresses the class existence requirement as an antecedent instead of a hypothesis.
|- (A e. B -> (rank` A) = |^|{x e. On | A e. (R1` suc x)})
 
Theoremrankval2 4663 Value of an alternate definition of the rank function. Definition of [BellMachover] p. 478.
|- (A e. B -> (rank` A) = |^|{x e. On | A (_ (R1` x)})
 
Theoremrankon 4664 The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79.
|- (rank` A) e. On
 
Theoremrankid 4665 Identity law for the rank function.
|- A e. V   =>   |- A e. (R1` suc (rank` A))
 
Theoremrankr1lem 4666 Lemma for rankr1 4667.
 
Theoremrankr1 4667 A relationship between the rank function and the cumulative hierarchy of sets function R1. Proposition 9.15(2) of [TakeutiZaring] p. 79.
|- A e. V   =>   |- (B = (rank` A) <-> (-. A e. (R1` B) /\ A e. (R1` suc B)))
 
Theoremrankr1g 4668 A relationship between the rank function and the cumulative hierarchy of sets function R1. Proposition 9.15(2) of [TakeutiZaring] p. 79.
|- (A e. C -> (B = (rank` A) <-> (-. A e. (R1` B) /\ A e. (R1` suc B))))
 
Theoremssrankr1 4669 A relationship between an ordinal number less than or equal to a rank, and the cumulative hierarchy of sets R1. Proposition 9.15(3) of [TakeutiZaring] p. 79.
|- A e. V   =>   |- (B e. On -> (B (_ (rank` A) <-> -. A e. (R1` B)))
 
Theoremrankr1a 4670 A relationship between rank and