mmtheorems47 - Metamath Proof Explorer

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-10687

Statement List for Metamath Proof Explorer - 4601-4700 - Page 47 of 107

Type	Label	Description
Statement
Theorem	inf3lemb 4601	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description.
Theorem	inf3lemc 4602	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description.
Theorem	inf3lemd 4603	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description.
Theorem	inf3lem1 4604	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description.
Theorem	inf3lem2 4605	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description.
Theorem	inf3lem3 4606	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 4587.
Theorem	inf3lem4 4607	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description.
Theorem	inf3lem5 4608	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description.
Theorem	inf3lem6 4609	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description.
Theorem	inf3lem7 4610	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4611 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of funrnex 3615.
Theorem	inf3 4611	Our Axiom of Infinity ax-inf 4613 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 4599, 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 4615 and zfinf 4617.) The main proof is provided by inf3lema 4600 through inf3lem7 4610, and this final piece eliminates the auxiliary hypothesis of inf3lem7 4610. 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 4601.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 4602.) 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 4604.) 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 4605.) 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 4606.) 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 4607.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 4608.) 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 4609.) 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 4610.) Q.E.D.
|- E.x(x =/= (/) /\ x (_ U.x)   =>   |- om e. V
Theorem	infeq5 4612	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 4618.) 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
Axiom	ax-inf 4613	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 4598 and inf2 4599). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf 4617 and omex 4618 and are based on the (nontrivial) proof of inf3 4611. Our version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 4616. Theorem inf0 4597 shows the reverse derivation of our axiom from a standard one. Theorem inf5 4619 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 4616 requires this axiom along with Regularity ax-reg 4584 for its derivation (as theorem axinf2 4615 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 4616 instead of this one.
|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
Theorem	axinf 4614	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)))
Theorem	axinf2 4615	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 4613 and Regularity ax-reg 4584. This theorem should not be referenced in any proof. Instead, use ax-inf2 4616 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)))))
Axiom	ax-inf2 4616	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 4617 shows it converted to abbreviations. This axiom was derived as theorem axinf2 4615 above, using our version of Infinity ax-inf 4613 and the Axiom of Regularity ax-reg 4584. We will reference ax-inf2 4616 instead of axinf2 4615 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)))))
Theorem	zfinf 4617	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 4616 for the unabbreviated version.)
|- E.x((/) e. x /\ A.y e. x suc y e. x)
Existence of omega (the set of natural numbers)
Theorem	omex 4618	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 4597. 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
Theorem	inf5 4619	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see theorem infeq5 4612). This provides us with a very compact way to express of the Axiom of Infinity using only elementary symbols.
|- E.x x (. U.x
Theorem	omelon 4620	Omega is an ordinal number.
|- om e. On
Theorem	dfom3 4621	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)}
Theorem	elom3 4622	A simplification of elom 3134 assuming the Axiom of Infinity.
|- (A e. om <-> A.x(Lim x -> A e. x))
Theorem	dfom4 4623	A simplification of df-om 3132 assuming the Axiom of Infinity.
|- om = {x | A.y(Lim y -> x e. y)}
Theorem	oancom 4624	Ordinal addition is not commutative. This theorem shows a counterexample. Remark in [TakeutiZaring] p. 60.
|- (1o +o om) =/= (om +o 1o)
Theorem	isfinite 4625	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)
Theorem	nnsdom 4626	A natural number is strictly dominated by the set of natural numbers.
|- (A e. om -> A ~< om)
Theorem	omenps 4627	Omega is equinumerous to a proper subset of itself. Example 13.2(4) of [Eisenberg] p. 216.
|- om ~~ (om \ {(/)})
Theorem	omensuc 4628	The set of natural numbers is equinumerous to its successor.
|- om ~~ suc om
Theorem	infensuc 4629	Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88.
|- ((A e. On /\ om (_ A) -> A ~~ suc A)
Theorem	unbnnt 4630	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 4538 eliminates its hypothesis by assuming the Axiom of Infinity.
|- ((A (_ om /\ A.x e. om E.y e. A x e. y) -> A ~~ om)
Theorem	noinfep 4631	Using the Axiom of Regularity in the form zfregfr 4592, 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
Syntax	cr1 4632	Extend class definition to include the cumulative hierarchy of sets function.
class R1
Syntax	crnk 4633	Extend class definition to include rank function.
class rank
Definition	df-r1 4634	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 4654). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 4642, r1suc 4643, and r1lim 4644. Theorem r1val1 4649 shows a recursive definition that works for all values, and theorems r1val2 4669 and r1val3 4670 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}, (/))
Definition	df-rank 4635	Define the rank function. See rankval 4659, rankval2 4661, rankval3 4672, or rankval4 4693 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 4663 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 4668.
|- rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}
Theorem	trcl 4636	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 4637 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))
Theorem	tz9.1 4637	Every set has a transitive closure (smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 4636 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))
Theorem	zfregs 4638	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) = (/))
Theorem	setind 4639	Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21.
|- (A.x(x (_ A -> x e. A) -> A = V)
Theorem	setind2 4640	Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996).
|- (P~A (_ A -> A = V)
Theorem	r1fnon 4641	The cumulative hierarchy of sets function is a function on the class of ordinal numbers.
|- R1 Fn On
Theorem	r10 4642	Value of the cumulative hierarchy of sets function at (/). Part of Definition 9.9 of [TakeutiZaring] p. 76.
|- (R1` (/)) = (/)
Theorem	r1suc 4643	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))
Theorem	r1lim 4644	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))
Theorem	r1tr 4645	The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202.
|- Tr (R1` A)
Theorem	r1ord 4646	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)))
Theorem	r1ord2 4647	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)))
Theorem	r1ord3 4648	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)))
Theorem	r1val1 4649	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))
Theorem	tz9.12lem1 4650	Lemma for tz9.12 4653.
Theorem	tz9.12lem2 4651	Lemma for tz9.12 4653.
Theorem	tz9.12lem3 4652	Lemma for tz9.12 4653.
Theorem	tz9.12 4653	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 4650 through tz9.12lem3 4652.
|- A e. V   =>   |- (A.x e. A E.y e. On x e. (R1` y) -> E.y e. On A e. (R1` y))
Theorem	tz9.13 4654	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)
Theorem	tz9.13g 4655	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 4654 expresses the class existence requirement as an antecedent.
|- (A e. B -> E.x e. On A e. (R1` x))
Theorem	rankwflem 4656	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 4655 is useful in proofs of theorems about the rank function.
|- (A e. B -> E.x e. On A e. (R1` suc x))
Theorem	jech9.3 4657	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
Theorem	unir1 4658	The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of [Mendelson] p. 281.
|- U.(R1"On) = V
Theorem	rankval 4659	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)}
Theorem	rankvalg 4660	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 4659 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)})
Theorem	rankval2 4661	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)})
Theorem	rankon 4662	The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79.
|- (rank` A) e. On
Theorem	rankid 4663	Identity law for the rank function.
|- A e. V   =>   |- A e. (R1` suc (rank` A))
Theorem	rankr1lem 4664	Lemma for rankr1 4665.
Theorem	rankr1 4665	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)))
Theorem	rankr1g 4666	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))))
Theorem	ssrankr1 4667	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)))
Theorem	rankr1a 4668	A relationship between rank and R1, clearly equivalent to ssrankr1 4667 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 4690 for the subset verion. (Contributed by Raph Levien, 29-May-2004.)
|- A e. V   =>   |- (B e. On -> (A e. (R1` B) <-> (rank` A) e. B))
Theorem	r1val2 4669	The value of the cumulative hierarchy of sets function expressed in terms of rank. Definition 15.19 of [Monk1] p. 113.
|- (A e. On -> (R1` A) = {x |