mmtheorems48 - 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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 4701-4800 - Page 48 of 123

Type	Label	Description
Statement
Theorem	unifi 4701	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144.
|- ((A e. Fin /\ A.x e. A x e. Fin) -> U.A e. Fin)
Theorem	unifi2 4702	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 4701 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 4693).
|- ((A ~< om /\ A.x e. A x ~< om) -> U.A ~< om)
Theorem	fiint 4703	Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite non-empty subcollection of A is in A." This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally.
|- (A.x e. A A.y e. A (x i^i y) e. A <-> A.x((x (_ A /\ x =/= (/) /\ x e. Fin) -> |^|x e. A))
Theorem	abfii1 4704	Two ways to express the collection of finite intersections of a set A.
|- |^|{x | (A (_ x /\ A.y e. x A.z e. x (y i^i z) e. x)} = |^|{x | (A (_ x /\ A.y((y (_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))}
Theorem	abfii2 4705	Two ways to express the collection of finite intersections of a set A.
|- A e. V   =>   |- {x | E.y(y (_ A /\ y e. Fin /\ x = |^|y)} = |^|{x | A.y((y (_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)}
Theorem	abfii3 4706	Two ways to express the collection of finite intersections of a set A.
|- A e. V   =>   |- |^|{x | (A (_ x /\ A.y((y (_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} = |^|{x | A.y((y (_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)}
Theorem	abfii4 4707	Two ways to express the collection of finite intersections of a set A. Even though the expressions differ by only one symbol, the proof is not simple.
|- A e. V   =>   |- |^|{x | (A (_ x /\ A.y((y (_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} = |^|{x | (A (_ x /\ A.y((y (_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))}
Theorem	abfii5 4708	Two ways to express the collection of finite intersections of a set A.
|- A e. V   =>   |- |^|{x | (A (_ x /\ A.y e. x A.z e. x (y i^i z) e. x)} = {x | E.y(y (_ A /\ y e. Fin /\ x = |^|y)}
Theorem	fodomfi 4709	An onto function implies dominance of domain over range, for finite sets. Unlike fodom 4944 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof.
|- ((A e. Fin /\ F:A-onto->B) -> B ~<_ A)
Theorem	fodomfib 4710	Equivalence of an onto mapping and dominance for a non-empty finite set. Unlike fodomb 4946 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof.
|- (A e. Fin -> ((A =/= (/) /\ E.f f:A-onto->B) <-> ((/) ~< B /\ B ~<_ A)))
Theorem	fofi 4711	If a function has a finite domain, its range is finite. Theorem 37 of [Suppes] p. 104.
|- ((A e. Fin /\ F:A-onto->B) -> B e. Fin)
Theorem	iunfi 4712	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 4701. Note that B depends on x, i.e. can be thought of as B(x).
|- ((A e. Fin /\ A.x e. A B e. Fin) -> U_x e. A B e. Fin)
Theorem	pwfilem 4713	Lemma for pwfi 4714.
Theorem	pwfi 4714	The power set of a finite set is finite and vice-versa. Theorem 38 of [Suppes] p. 104 and its converse, Theorem 40 of [Suppes] p. 105.
|- (A e. Fin <-> P~A e. Fin)
Theorem	pm54.43 4715	Theorem *54.43 of [WhiteheadRussell] p. 360. "From this proposition it will follow, when arithmetical addition has been defined, that 1+1=2." See http://en.wikipedia.org/wiki/Principia_Mathematica#Quotations. This theorem states that two sets of cardinality 1 are disjoint iff their union has cardinality 2. Whitehead and Russell define 1 as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 4981), so that their A e. 1 means, in our notation, A e. {x | (card` x) = 1o} i.e. (card` A) = 1o (by elab 1943) i.e. A ~~ 1o (by carden 4979 and cardnn 4970). We do not have several of their earlier lemmas available (which would otherwise be unused by our different approach to arithmetic), so our proof is longer. (It is also longer because we must show every detail.) Theorem pm110.643 5074 shows the derivation of 1+1=2 for cardinal numbers from this theorem.
|- ((A ~~ 1o /\ B ~~ 1o) -> ((A i^i B) = (/) <-> (A u. B) ~~ 2o))
Supremum
Syntax	csup 4716	Extend class notation to include supremum of class A. Here R is ordinarily a relation that strictly orders class B. For example, R could be 'less than' and B could be the set of real numbers.
class sup(A, B, R)
Definition	df-sup 4717	Define the supremum of class B. It is meaningful when R is a relation that strictly orders A and when the supremum exists. For example, R could be 'less than', A could be the set of real numbers, and B could be the set of all positive reals whose square is less than 2; in this case the supremum is defined as the square root of 2 per sqrval 6872. We will also use this notation for "infimum" by replacing R with `'R.
|- sup(B, A, R) = U.{x e. A | (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))}
Theorem	supeq1 4718	Equality theorem for supremum.
|- (B = C -> sup(B, A, R) = sup(C, A, R))
Theorem	supmo 4719	Any class B has at most one supremum in A (where R is interpreted as 'less than').
|- R Or A   =>   |- E*x(x e. A /\ (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)))
Theorem	supex 4720	A supremum is a set.
|- R Or A   =>   |- sup(B, A, R) e. V
Theorem	supeu 4721	A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general).
|- R Or A   =>   |- (E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)) -> E!x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)))
Theorem	supcl 4722	A supremum belongs to its base class (closure law).
|- R Or A   =>   |- (E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)) -> sup(B, A, R) e. A)
Theorem	supub 4723	A supremum is an upper bound.
|- R Or A   =>   |- (E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)) -> (C e. B -> -. sup(B, A, R)RC))
Theorem	suplub 4724	A supremum is the least upper bound.
|- R Or A   =>   |- (E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)) -> ((C e. A /\ CRsup(B, A, R)) -> E.z e. B CRz))
Theorem	supnub 4725	An upper bound is not less than the supremum.
|- R Or A   =>   |- (E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)) -> ((C e. A /\ A.z e. B -. CRz) -> -. CRsup(B, A, R)))
Theorem	supeui 4726	A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general).
|- R Or A   &   |- E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))   =>   |- E!x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))
Theorem	supcli 4727	A supremum belongs to its base class (closure law).
|- R Or A   &   |- E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))   =>   |- sup(B, A, R) e. A
Theorem	supubi 4728	A supremum is an upper bound.
|- R Or A   &   |- E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))   =>   |- (C e. B -> -. sup(B, A, R)RC)
Theorem	suplubi 4729	A supremum is the least upper bound.
|- R Or A   &   |- E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))   =>   |- ((C e. A /\ CRsup(B, A, R)) -> E.z e. B CRz)
Theorem	supnubi 4730	An upper bound is not less than the supremum.
|- R Or A   &   |- E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))   =>   |- ((C e. A /\ A.z e. B -. CRz) -> -. CRsup(B, A, R))
Theorem	supmaxlem 4731	A set that contains a greatest element satisfies the antecedent in supremum theorems. This allows sup(A, B, R) to be used in some situations without the completeness axiom. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- ((C e. A /\ C e. B /\ A.z e. B -. CRz) -> E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)))
Theorem	supmax 4732	The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- R Or A   =>   |- ((C e. A /\ C e. B /\ A.y e. B -. CRy) -> sup(B, A, R) = C)
Theorem	suppr 4733	The supremum of a pair.
|- R Or A   =>   |- ((B e. A /\ C e. A) -> sup({B, C}, A, R) = if(CRB, B, C))
Theorem	supsn 4734	The supremum of a singleton.
|- R Or A   =>   |- (B e. A -> sup({B}, A, R) = B)
Theorem	supsnALT 4735	The supremum of a singleton. This version of supsn 4734 is proved directly.
|- R Or A   =>   |- (B e. A -> sup({B}, A, R) = B)
ZF Set Theory - add the Axiom of Regularity
Introduce the Axiom of Regularity
Axiom	ax-reg 4736	Axiom of Regularity. An axiom of Zermelo-Fraenkel set theory. Also called the Axiom of Foundation. A rather non-intuitive axiom that denies more than it asserts, it states (in the form of zfreg 4739) that every non-empty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 4741). A stronger version that works for proper classes is proved as zfregs 4793.
|- (E.y y e. x -> E.y(y e. x /\ A.z(z e. y -> -. z e. x)))
Theorem	axreg 4737	Axiom of Regularity expressed more compactly.
|- (x e. y -> E.x(x e. y /\ A.z(z e. x -> -. z e. y)))
Theorem	zfregcl 4738	The Axiom of Regularity with class variables.
|- A e. V   =>   |- (E.x x e. A -> E.x e. A A.y e. x -. y e. A)
Theorem	zfreg 4739	The Axiom of Regularity using abbreviations. Axiom 6 of [TakeutiZaring] p. 21. This is called the "weak form." There is also a "strong form," not requiring that A be a set, that can be proved with more difficulty (see zfregs 4793).
|- A e. V   =>   |- (A =/= (/) -> E.x e. A (x i^i A) = (/))
Theorem	zfreg2 4740	The Axiom of Regularity using abbreviations. This form with the intersection arguments commuted (compared to zfreg 4739) is formally more convenient for us in some cases. Axiom Reg of [BellMachover] p. 480.
|- A e. V   =>   |- (A =/= (/) -> E.x e. A (A i^i x) = (/))
Theorem	elirrv 4741	The membership relation is irreflexive: no set is a member of itself. Theorem 105 of [Suppes] p. 54. (This is trivial to prove from zfregfr 4746 and efrirr 2957, but this proof is direct from the Axiom of Regularity.)
|- -. x e. x
Theorem	elirr 4742	No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22.
|- -. A e. A
Theorem	sucprcreg 4743	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	ruv 4744	The Russell class is equal to the universe V. Exercise 5 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 4-Oct-2008.)
|- {x | x e/ x} = V
Theorem	ruALT 4745	Alternate proof of Russell's Paradox ru 1984, simplified using (indirectly) the Axiom of Regularity ax-reg 4736. (Contributed by Alan Sare, 4-Oct-2008.)
|- {x | x e/ x} e/ V
Theorem	zfregfr 4746	The epsilon relation is founded on any class.
|- E Fr A
Theorem	en2lp 4747	No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206.
|- -. (A e. B /\ B e. A)
Theorem	preleq 4748	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 4749	Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 4736 (via the preleq 4748 step). See df-op 2474 for a description of other ordered pair representations. 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 4750	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 4751	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 4767.
|- om e. V   =>   |- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
Theorem	inf1 4752	Variation of Axiom of Infinity (using zfinf 4768 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 4753	Variation of Axiom of Infinity. There exists a non-empty set that is a subset of its union (using zfinf 4768 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 4754	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description.
Theorem	inf3lemb 4755	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description.
Theorem	inf3lemc 4756	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description.
Theorem	inf3lemd 4757	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description.
Theorem	inf3lem1 4758	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description.
Theorem	inf3lem2 4759	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description.
Theorem	inf3lem3 4760	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 4739.
Theorem	inf3lem4 4761	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description.
Theorem	inf3lem5 4762	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description.
Theorem	inf3lem6 4763	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description.
Theorem	inf3lem7 4764	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4765 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of funrnex 3720.
Theorem	inf3 4765	Our Axiom of Infinity ax-inf 4767 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 4753, 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 4769 and zfinf2 4771.) The main proof is provided by inf3lema 4754 through inf3lem7 4764, and this final piece eliminates the auxiliary hypothesis of inf3lem7 4764. 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 4755.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 4756.) 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 4758.) 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 4759.) 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 4760.) 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 4761.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 4762.) 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 4763.) 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 4764.) Q.E.D.
|- E.x(x =/= (/) /\ x (_ U.x)   =>   |- om e. V
Theorem	infeq5 4766	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 4772.) 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 4767	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 4752 and inf2 4753). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf2 4771 and omex 4772 and are based on the (nontrivial) proof of inf3 4765. Our version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 4770. Theorem inf0 4751 shows the reverse derivation of our axiom from a standard one. Theorem inf5 4774 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 1009 and ax-9 1001) that at least one thing exists. The standard version of Infinity ax-inf2 4770 requires this axiom along with Regularity ax-reg 4736 for its derivation (as theorem axinf2 4769 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 4770 instead of this one. The derivation of this axiom from ax-inf2 4770 is shown by theorem axinf 4773.
|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
Theorem	zfinf 4768	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 4769	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 4767 and Regularity ax-reg 4736. This theorem should not be referenced in any proof. Instead, use ax-inf2 4770 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 4770	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 zfinf2 4771 shows it converted to abbreviations. This axiom was derived as theorem axinf2 4769 above, using our version of Infinity ax-inf 4767 and the Axiom of Regularity ax-reg 4736. We will reference ax-inf2 4770 instead of axinf2 4769 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 4767 from ax-inf2 4770 is shown by theorem axinf 4773.
|- 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	zfinf2 4771	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 4770 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 4772	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 4751. 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 3230 and onprc 3143. 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 3237 through peano5 3241 (which many textbooks prove more easily assuming Infinity).
|- om e. V
Theorem	axinf 4773	The first version of the Axiom of Infinity ax-inf 4767 proved from the second version ax-inf2 4770.
|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
Theorem	inf5 4774	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see theorem infeq5 4766). 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 4775	Omega is an ordinal number.
|- om e. On
Theorem	dfom3 4776	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 4777	A simplification of elom 3221 assuming the Axiom of Infinity.
|- (A e. om <-> A.x(Lim x -> A e. x))
Theorem	dfom4 4778	A simplification of df-om 3219 assuming the Axiom of Infinity.
|- om = {x | A.y(Lim y -> x e. y)}
Theorem	oancom 4779	Ordinal addition is not commutative. This theorem shows a counterexample. Remark in [TakeutiZaring] p. 60.
|- (1o +o om) =/= (om +o 1o)
Theorem	isfinite 4780	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 <-> A e. Fin)
Theorem	nnsdom 4781	A natural number is strictly dominated by the set of natural numbers.
|- (A e. om -> A ~< om)
Theorem	omenps 4782	Omega is equinumerous to a proper subset of itself. Example 13.2(4) of [Eisenberg] p. 216.
|- om ~~ (om \ {(/)})
Theorem	omensuc 4783	The set of natural numbers is equinumerous to its successor.
|- om ~~ suc om
Theorem	infensuc 4784	Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88.
|- ((A e. On /\ om (_ A) -> A ~~ suc A)
Theorem	unbnn3 4785	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 4690 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 4786	Using the Axiom of Regularity in the form zfregfr 4746, 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 4787	Extend class definition to include the cumulative hierarchy of sets function.
class R1
Syntax	crnk 4788	Extend class definition to include rank function.
class rank
Definition	df-r1 4789	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 4809). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 4797, r1suc 4798, and r1lim 4799. Theorem r1val1 4804 shows a recursive definition that works for all values, and theorems r1val2 4824 and r1val3 4825 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 4790	Define the rank function. See rankval 4814, rankval2 4816, rankval3 4827, or rankval4 4848 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 4818 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 4823.
|- rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}
Theorem	trcl 4791	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 4792 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 4792	Every set has a transitive closure (smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 4791 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 4793	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 4794	Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21.
|- (A.x(x (_ A -> x e. A) -> A = V)
Theorem	setind2 4795	Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996).
|- (P~A (_ A -> A = V)
Theorem	r1fnon 4796	The cumulative hierarchy of sets function is a function on the class of ordinal numbers.
|- R1 Fn On
Theorem	r10 4797	Value of the cumulative hierarchy of sets function at (/). Part of Definition 9.9 of [TakeutiZaring] p. 76.
|- (R1` (/)) = (/)
Theorem	r1suc 4798	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 4799	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 4800	The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202.
|- Tr (R1` A)