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-10700 108 10701-10789

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

Type	Label	Description
Statement
Theorem	elirr 4601	No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22.
|- -. A e. A
Theorem	sucprcreg 4602	A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity).
|- (-. A e. V <-> suc A = A)
Theorem	zfregfr 4603	The epsilon relation is founded on any class.
|- E Fr A
Theorem	en2lp 4604	No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206.
|- -. (A e. B /\ B e. A)
Theorem	preleq 4605	Equality of two unordered pairs when one member of each pair contains the other member.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   =>   |- (((A e. B /\ C e. D) /\ {A, B} = {C, D}) -> (A = C /\ B = D))
Theorem	opthreg 4606	Theorem for alternate representation of ordered pairs, requiring Regularity. Exercise 34 of [Enderton] p. 207.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   =>   |- ({A, {A, B}} = {C, {C, D}} <-> (A = C /\ B = D))
Theorem	suc11reg 4607	The successor operation behaves like a one-to-one function (assuming the Axiom of Regularity). Exercise 35 of [Enderton] p. 208 and its converse.
|- (suc A = suc B <-> A = B)
Axiom of Infinity equivalents
Theorem	inf0 4608	Our Axiom of Infinity derived from existence of omega. The proof shows that the especially contrived class "ran (rec({<.v, u>. | u = suc v}, x) |` om)" exists, is a subset of its union, and contains a given set x (and thus is non-empty). Thus it provides an example demonstrating that a set y exists with the necessary properties demanded by ax-inf 4624.
|- om e. V   =>   |- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
Theorem	inf1 4609	Variation of Axiom of Infinity (using axinf 4625 as a hypothesis). 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 =/= (/) /\ A.y(y e. x -> E.z(y e. z /\ z e. x)))
Theorem	inf2 4610	Variation of Axiom of Infinity. There exists a non-empty set that is a subset of its union (using axinf 4625 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)
Theorem	inf3lema 4611	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description.
Theorem	inf3lemb 4612	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description.
Theorem	inf3lemc 4613	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description.
Theorem	inf3lemd 4614	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description.
Theorem	inf3lem1 4615	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description.
Theorem	inf3lem2 4616	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description.
Theorem	inf3lem3 4617	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 4598.
Theorem	inf3lem4 4618	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description.
Theorem	inf3lem5 4619	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description.
Theorem	inf3lem6 4620	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description.
Theorem	inf3lem7 4621	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4622 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of funrnex 3613.
Theorem	inf3 4622	Our Axiom of Infinity ax-inf 4624 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 4610, 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 4626 and zfinf 4628.) The main proof is provided by inf3lema 4611 through inf3lem7 4621, and this final piece eliminates the auxiliary hypothesis of inf3lem7 4621. 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-1996, 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 4612.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 4613.) 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 4615.) 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 4616.) 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 4617.) 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 4618.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 4619.) 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 4620.) 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 4621.) Q.E.D.
|- E.x(x =/= (/) /\ x (_ U.x)   =>   |- om e. V
Theorem	infeq5 4623	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 4629.) 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 4624	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 4609 and inf2 4610). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf 4628 and omex 4629 and are based on the (nontrivial) proof of inf3 4622. Our version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 4627. Theorem inf0 4608 shows the reverse derivation of our axiom from a standard one. Theorem inf5 4630 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 973 and ax-9 965) that at least one thing exists. The standard version of Infinity ax-inf2 4627 requires this axiom along with Regularity ax-reg 4595 for its derivation (as theorem axinf2 4626 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 4627 instead of this one.
|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
Theorem	axinf 4625	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 4626	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 4624 and Regularity ax-reg 4595. This theorem should not be referenced in any proof. Instead, use ax-inf2 4627 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 4627	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 4628 shows it converted to abbreviations. This axiom was derived as theorem axinf2 4626 above, using our version of Infinity ax-inf 4624 and the Axiom of Regularity ax-reg 4595. We will reference ax-inf2 4627 instead of axinf2 4626 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 4628	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 4627 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 4629	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 4608. 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 4630	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see theorem infeq5 4623). 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 4631	Omega is an ordinal number.
|- om e. On
Theorem	dfom3 4632	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 4633	A simplification of elom 3134 assuming the Axiom of Infinity.
|- (A e. om <-> A.x(Lim x -> A e. x))
Theorem	dfom4 4634	A simplification of df-om 3132 assuming the Axiom of Infinity.
|- om = {x | A.y(Lim y -> x e. y)}
Theorem	oancom 4635	Ordinal addition is not commutative. This theorem shows a counterexample. Remark in [TakeutiZaring] p. 60.
|- (1o +o om) =/= (om +o 1o)
Theorem	isfiniteOLD 4636	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 4637	A natural number is strictly dominated by the set of natural numbers.
|- (A e. om -> A ~< om)
Theorem	omenps 4638	Omega is equinumerous to a proper subset of itself. Example 13.2(4) of [Eisenberg] p. 216.
|- om ~~ (om \ {(/)})
Theorem	omensuc 4639	The set of natural numbers is equinumerous to its successor.
|- om ~~ suc om
Theorem	infensuc 4640	Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88.
|- ((A e. On /\ om (_ A) -> A ~~ suc A)
Theorem	unbnnt 4641	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 4546 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 4642	Using the Axiom of Regularity in the form zfregfr 4603, 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 4643	Extend class definition to include the cumulative hierarchy of sets function.
class R1
Syntax	crnk 4644	Extend class definition to include rank function.
class rank
Definition	df-r1 4645	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 4665). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 4653, r1suc 4654, and r1lim 4655. Theorem r1val1 4660 shows a recursive definition that works for all values, and theorems r1val2 4680 and r1val3 4681 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 4646	Define the rank function. See rankval 4670, rankval2 4672, rankval3 4683, or rankval4 4704 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 4674 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 4679.
|- rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}
Theorem	trcl 4647	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 4648 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 4648	Every set has a transitive closure (smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 4647 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 4649	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 4650	Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21.
|- (A.x(x (_ A -> x e. A) -> A = V)
Theorem	setind2 4651	Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996).
|- (P~A (_ A -> A = V)
Theorem	r1fnon 4652	The cumulative hierarchy of sets function is a function on the class of ordinal numbers.
|- R1 Fn On
Theorem	r10 4653	Value of the cumulative hierarchy of sets function at (/). Part of Definition 9.9 of [TakeutiZaring] p. 76.
|- (R1` (/)) = (/)
Theorem	r1suc 4654	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 4655	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 4656	The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202.
|- Tr (R1` A)
Theorem	r1ord 4657	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 4658	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 4659	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 4660	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 4661	Lemma for tz9.12 4664.
Theorem	tz9.12lem2 4662	Lemma for tz9.12 4664.
Theorem	tz9.12lem3 4663	Lemma for tz9.12 4664.
Theorem	tz9.12 4664	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 4661 through tz9.12lem3 4663.
|- 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 4665	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 4666	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 4665 expresses the class existence requirement as an antecedent.
|- (A e. B -> E.x e. On A e. (R1` x))
Theorem	rankwflem 4667	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 4666 is useful in proofs of theorems about the rank function.
|-