mmtheorems58 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 5701-5800 - Page 58 of 175

Type	Label	Description
Statement
Theorem	elirr 5701	No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
|- -. A e. A
Theorem	elirrOLD 5702	No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22.
|- -. A e. A
Theorem	sucprcreg 5703	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 5704	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 5705	Alternate proof of Russell's Paradox ru 2451, simplified using (indirectly) the Axiom of Regularity ax-reg 5695. (Contributed by Alan Sare, 4-Oct-2008.)
|- {x | x e/ x} e/ _V
Theorem	zfregfr 5706	The epsilon relation is founded on any class.
|- _E Fr A
Theorem	en2lp 5707	No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206.
|- -. (A e. B /\ B e. A)
Theorem	preleq 5708	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 5709	Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 5695 (via the preleq 5708 step). See df-op 3053 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 5710	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)
Theorem	dford2 5711	Assuming ax-reg 5695, an ordinal is a transitive class on which inclusion satisfies trichotomy. (Contributed by Scott Fenton, 27-Oct-2010.)
|- (Ord A <-> (Tr A /\ A.x e. A A.y e. A (x e. y \/ x = y \/ y e. x)))
Axiom of Infinity equivalents
Theorem	inf0 5712	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) " exi sts, 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 5728.
|- om e. _V   =>   |- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
Theorem	inf1 5713	Variation of Axiom of Infinity (using zfinf 5729 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 5714	Variation of Axiom of Infinity. There exists a non-empty set that is a subset of its union (using zfinf 5729 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 C_ U.x)
Theorem	inf3lema 5715	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description.
Theorem	inf3lemb 5716	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description.
Theorem	inf3lemc 5717	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description.
Theorem	inf3lemd 5718	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description.
Theorem	inf3lem1 5719	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description.
Theorem	inf3lem2 5720	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description.
Theorem	inf3lem3 5721	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 5698.
Theorem	inf3lem4 5722	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description.
Theorem	inf3lem5 5723	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description.
Theorem	inf3lem6 5724	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description.
Theorem	inf3lem7 5725	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 5726 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of funrnex 4544.
Theorem	inf3 5726	Our Axiom of Infinity ax-inf 5728 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 5714, 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 5730 and zfinf2 5732.) The main proof is provided by inf3lema 5715 through inf3lem7 5725, and this final piece eliminates the auxiliary hypothesis of inf3lem7 5725. 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 5716.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 5717.) 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 5719.) 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 5720.) 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 5721.) 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 5722.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 5723.) 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 5724.) 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 5725.) Q.E.D.
|- E.x(x =/= (/) /\ x C_ U.x)   =>   |- om e. _V
Theorem	infeq5 5727	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 5733.) 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 C. U.x <-> om e. _V)
ZF Set Theory - add the Axiom of Infinity
Introduce the Axiom of Infinity
Axiom	ax-inf 5728	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 5713 and inf2 5714). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf2 5732 and omex 5733 and are based on the (nontrivial) proof of inf3 5726. Our version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 5731. Theorem inf0 5712 shows the reverse derivation of our axiom from a standard one. Theorem inf5 5735 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 1319 and ax-9 1307) that at least one thing exists. The standard version of Infinity ax-inf2 5731 requires this axiom along with Regularity ax-reg 5695 for its derivation (as theorem axinf2 5730 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 5731 instead of this one. The derivation of this axiom from ax-inf2 5731 is shown by theorem axinf 5734.
|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
Theorem	zfinf 5729	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 5730	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 5728 and Regularity ax-reg 5695. This theorem should not be referenced in any proof. Instead, use ax-inf2 5731 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 5731	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 5732 shows it converted to abbreviations. This axiom was derived as theorem axinf2 5730 above, using our version of Infinity ax-inf 5728 and the Axiom of Regularity ax-reg 5695. We will reference ax-inf2 5731 instead of axinf2 5730 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 5728 from ax-inf2 5731 is shown by theorem axinf 5734.
|- 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 5732	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 5731 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 5733	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 5712. 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 3963 and onprc 3865. 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 3971 through peano5 3975 (which many textbooks prove more easily assuming Infinity).
|- om e. _V
Theorem	axinf 5734	The first version of the Axiom of Infinity ax-inf 5728 proved from the second version ax-inf2 5731.
|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
Theorem	inf5 5735	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see theorem infeq5 5727). This provides us with a very compact way to express of the Axiom of Infinity using only elementary symbols.
|- E.x x C. U.x
Theorem	omelon 5736	Omega is an ordinal number.
|- om e. On
Theorem	dfom3 5737	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 5738	A simplification of elom 3952 assuming the Axiom of Infinity.
|- (A e. om <-> A.x(Lim x -> A e. x))
Theorem	dfom4 5739	A simplification of df-om 3950 assuming the Axiom of Infinity.
|- om = {x | A.y(Lim y -> x e. y)}
Theorem	oancom 5740	Ordinal addition is not commutative. This theorem shows a counterexample. Remark in [TakeutiZaring] p. 60.
|- (1o +o om) =/= (om +o 1o)
Theorem	isfinite 5741	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 5742	A natural number is strictly dominated by the set of natural numbers.
|- (A e. om -> A ~< om)
Theorem	omenps 5743	Omega is equinumerous to a proper subset of itself. Example 13.2(4) of [Eisenberg] p. 216.
|- om ~~ (om \ {(/)})
Theorem	omensuc 5744	The set of natural numbers is equinumerous to its successor.
|- om ~~ suc om
Theorem	infensuc 5745	Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88.
|- ((A e. On /\ om C_ A) -> A ~~ suc A)
Theorem	unbnn3 5746	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 5637 eliminates its hypothesis by assuming the Axiom of Infinity.
|- ((A C_ om /\ A.x e. om E.y e. A x e. y) -> A ~~ om)
Theorem	noinfep 5747	Using the Axiom of Regularity in the form zfregfr 5706, 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 5748	Extend class definition to include the cumulative hierarchy of sets function.
class R1
Syntax	crnk 5749	Extend class definition to include rank function.
class rank
Definition	df-r1 5750	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 5774). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 5762, r1suc 5763, and r1lim 5764. Theorem r1val1 5769 shows a recursive definition that works for all values, and theorems r1val2 5789 and r1val3 5790 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 = ~Px}, (/))
Definition	df-rank 5751	Define the rank function. See rankval 5779, rankval2 5781, rankval3 5792, or rankval4 5813 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 5783 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 5788.
|- rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}
Theorem	trcl 5752	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 5753 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_ C /\ Tr C /\ A.x((A C_ x /\ Tr x) -> C C_ x))
Theorem	tz9.1 5753	Every set has a transitive closure (smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 5752 for an explicit expression for the transitive closure. Apparently open problems are whether this theorem can be proved without the Axiom of Infinity; if not, then whether it implies Infinity; and if not, what is the "property" that Infinity has that the other axioms don't have that is weaker than Infinity itself? (Added 22-Mar-2011) The following article seems to answer the first question, that it can't be proved without Infinity, in the affirmative: Mancini, Antonella and Zambella, Domenico (2001). "A note on recursive models of set theories." Notre Dame Journal of Formal Logic, 42(2):109-115. (Thanks to Scott Fenton.)
|- A e. _V   =>   |- E.x(A C_ x /\ Tr x /\ A.y((A C_ y /\ Tr y) -> x C_ y))
Theorem	zfregs 5754	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	zfregs2 5755	Alternate strong form of the Axiom of Regularity. Not every element of a non-empty class contains some element of that class. This proof was automatically generated from the virtual deduction proof zfregs2VD 16665 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
|- (A =/= (/) -> -. A.x e. A E.y(y e. A /\ y e. x))
Theorem	en3lplem1 5756	Lemma for en3lp 5758. This proof was automatically generated from the virtual deduction proof en3lplem1VD 16667 using a translation program. (Contributed by Alan Sare, 24-Oct-2011)
Theorem	en3lplem2 5757	Lemma for en3lp 5758. This proof was automatically generated from the virtual deduction proof en3lplem2VD 16668 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
Theorem	en3lp 5758	No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD 16669 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
|- -. (A e. B /\ B e. C /\ C e. A)
Theorem	setind 5759	Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21.
|- (A.x(x C_ A -> x e. A) -> A = _V)
Theorem	setind2 5760	Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996).
|- (~PA C_ A -> A = _V)
Theorem	r1fnon 5761	The cumulative hierarchy of sets function is a function on the class of ordinal numbers.
|- R1 Fn On
Theorem	r10 5762	Value of the cumulative hierarchy of sets function at (/). Part of Definition 9.9 of [TakeutiZaring] p. 76.
|- (R1` (/)) = (/)
Theorem	r1suc 5763	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 5764	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 5765	The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202.
|- Tr (R1` A)
Theorem	r1ord 5766	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 5767	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) C_ (R1` B)))
Theorem	r1ord3 5768	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 C_ B -> (R1` A) C_ (R1` B)))
Theorem	r1val1 5769	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 5770	Lemma for tz9.12 5773.
Theorem	tz9.12lem2 5771	Lemma for tz9.12 5773.
Theorem	tz9.12lem3 5772	Lemma for tz9.12 5773.
Theorem	tz9.12 5773	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 5770 through tz9.12lem3 5772.
|- 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 5774	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 5775	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 5774 expresses the class existence requirement as an antecedent.
|- (A e. B -> E.x e. On A e. (R1` x))
Theorem	rankwflem 5776	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 5775 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 5777	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 5778	The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of [Mendelson] p. 281.
|- U.(R1"On) = _V
Theorem	rankval 5779	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 5780	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 5779 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 5781	Value of an alternate definition of the rank function. Definition of [BellMachover] p. 478.
|- (A e. B -> (rank` A) = |^|{x e. On | A C_ (R1` x)})
Theorem	rankon 5782	The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79.
|- (rank` A) e. On
Theorem	rankid 5783	Identity law for the rank function.
|- A e. _V   =>   |- A e. (R1` suc (rank` A))
Theorem	rankr1lem 5784	Lemma for rankr1 5785.
Theorem	rankr1 5785	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 5786	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 5787	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 C_ (rank` A) <-> -. A e. (R1` B)))
Theorem	rankr1a 5788	A relationship between rank and R1, clearly equivalent to ssrankr1 5787 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 5810 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 5789	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 | (rank` x) e. A})
Theorem	r1val3 5790	The value of the cumulative hierarchy of sets function expressed in terms of rank. Theorem 15.18 of [Monk1] p. 113.
|- (A e. On -> (R1` A) = U_x e. A ~P{y | (rank` y) e. x})
Theorem	rankel 5791	The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79.
|- B e. _V   =>   |- (A e. B -> (rank` A) e. (rank` B))
Theorem	rankval3 5792	The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79.
|- A e. _V   =>   |- (rank` A) = |^|{x e. On | A.y e. A (rank` y) e. x}
Theorem	bndrank 5793	Any class whose elements have bounded rank is a set. Proposition 9.19 of [TakeutiZaring] p. 80.
|- (E.x e. On A.y e. A (rank` y) C_ x -> A e. _V)
Theorem	unbndrank 5794	The elements of a proper class have unbounded rank. Exercise 2 of [TakeutiZaring] p. 80.
|- (-. A e. _V -> A.x e. On E.y e. A x e. (rank` y))
Theorem	rankpw 5795	The rank of a power set. Part of Exercise 30 of [Enderton] p. 207.
|- A e. _V   =>   |- (rank` ~PA) = suc (rank` A)
Theorem	ranklim 5796	The rank of a set belongs to a limit ordinal iff the rank of its power set does.
|- (Lim B -> ((rank` A) e. B <-> (rank` ~PA) e. B))
Theorem	r1pw 5797	A stronger property of R1 than rankpw 5795. The latter merely proves that R1 of the successor is a power set, but here we prove that if A is in the cumulative hierarchy, then ~PA is in the cumulative hierarchy of the successor. (Contributed by Raph Levien, 29-May-2004.)
|- (B e. On -> (A e. (R1` B) <-> ~PA e. (R1` suc B)))
Theorem	r1pwcl 5798	The cumulative hierarchy of a limit ordinal is closed under power set. (Contributed by Raph Levien, 29-May-2004.)
|- (Lim B -> (A e. (R1` B) <-> ~PA e. (R1` B)))
Theorem	rankss 5799	The subset relation is inherited by the rank function. Exercise 1 of [TakeutiZaring] p. 80.
|- B e. _V   =>   |- (A C_ B -> (rank` A) C_ (rank` B))
Theorem	ranksn 5800	The rank of a singleton. Theorem 15.17(v) of [Monk1] p. 112.
|- A e. _V   =>   |- (rank` {A}) = suc (rank` A)