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

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

Type	Label	Description
Statement
Theorem	inf3lem6 4601	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4603 for detailed description.
Theorem	inf3lem7 4602	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 4603 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of funrnex 3608.
Theorem	inf3 4603	Our Axiom of Infinity ax-inf 4605 implies the standard Axiom of Infinity. The hypothesis is a variant of our Axiom of Infinity provided by inf2 4591, 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 4607 and zfinf 4609.) The main proof is provided by inf3lema 4592 through inf3lem7 4602, and this final piece eliminates the auxiliary hypothesis of inf3lem7 4602. 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 4593.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 4594.) 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 4596.) 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 4597.) 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 4598.) 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 4599.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 4600.) 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 4601.) 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 4602.) Q.E.D.
⊢ ∃x(x ≠ ∅ ⋀ x ⊆ ∪x)    ⇒   ⊢ ω ∈ V
Theorem	infeq5 4604	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 4610.) 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.
⊢ (∃x x ⊂ ∪x ↔ ω ∈ V)
ZF Set Theory - add the Axiom of Infinity
Introduce the Axiom of Infinity
Axiom	ax-inf 4605	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 4590 and inf2 4591). More standard versions, which essentially state that there exists a set containing all the natural numbers, are shown as zfinf 4609 and omex 4610 and are based on the (nontrivial) proof of inf3 4603. Our version has the advantage that when expanded to primitives, it has fewer symbols than the standard version ax-inf2 4608. Theorem inf0 4589 shows the reverse derivation of our axiom from a standard one. Theorem inf5 4611 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 972 and ax-9 964) that at least one thing exists. The standard version of Infinity ax-inf2 4608 requires this axiom along with Regularity ax-reg 4576 for its derivation (as theorem axinf2 4607 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 4608 instead of this one.
⊢ ∃y(x ∈ y ⋀ ∀z(z ∈ y → ∃w(z ∈ w ⋀ w ∈ y)))
Theorem	axinf 4606	Axiom of Infinity expressed with fewest number of different variables.
⊢ ∃x(y ∈ x ⋀ ∀y(y ∈ x → ∃z(y ∈ z ⋀ z ∈ x)))
Theorem	axinf2 4607	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 4605 and Regularity ax-reg 4576. This theorem should not be referenced in any proof. Instead, use ax-inf2 4608 below so that the ordinary uses of Regularity can be more easily identified.
⊢ ∃x(∃y(y ∈ x ⋀ ∀z ¬ z ∈ y) ⋀ ∀y(y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))))
Axiom	ax-inf2 4608	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 4609 shows it converted to abbreviations. This axiom was derived as theorem axinf2 4607 above, using our version of Infinity ax-inf 4605 and the Axiom of Regularity ax-reg 4576. We will reference ax-inf2 4608 instead of axinf2 4607 so that the ordinary uses of Regularity can be more easily identified.
⊢ ∃x(∃y(y ∈ x ⋀ ∀z ¬ z ∈ y) ⋀ ∀y(y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))))
Theorem	zfinf 4609	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 4608 for the unabbreviated version.)
⊢ ∃x(∅ ∈ x ⋀ ∀y ∈ x suc y ∈ x)
Existence of omega (the set of natural numbers)
Theorem	omex 4610	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 4589. A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial ¬ ω ∈ V; this would lead to ω = On (the proper class of ordinals) by omon 3139 and onprc 2985. 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 3145 through peano5 3149 (which many textbooks prove more easily assuming Infinity).
⊢ ω ∈ V
Theorem	inf5 4611	The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see theorem infeq5 4604). This provides us with a very compact way to express of the Axiom of Infinity using only elementary symbols.
⊢ ∃x x ⊂ ∪x
Theorem	omelon 4612	Omega is an ordinal number.
⊢ ω ∈ On
Theorem	dfom3 4613	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.
⊢ ω = ∩{x∣(∅ ∈ x ⋀ ∀y ∈ x suc y ∈ x)}
Theorem	elom3 4614	A simplification of elom 3130 assuming the Axiom of Infinity.
⊢ (A ∈ ω ↔ ∀x(Lim x → A ∈ x))
Theorem	dfom4 4615	A simplification of df-om 3128 assuming the Axiom of Infinity.
⊢ ω = {x∣∀y(Lim y → x ∈ y)}
Theorem	oancom 4616	Ordinal addition is not commutative. This theorem shows a counterexample. Remark in [TakeutiZaring] p. 60.
⊢ (1o +o ω) ≠ (ω +o 1o)
Theorem	isfinite 4617	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 ≺ ω ↔ ∃x ∈ ω A ≈ x)
Theorem	nnsdom 4618	A natural number is strictly dominated by the set of natural numbers.
⊢ (A ∈ ω → A ≺ ω)
Theorem	omenps 4619	Omega is equinumerous to a proper subset of itself. Example 13.2(4) of [Eisenberg] p. 216.
⊢ ω ≈ (ω ∖ {∅})
Theorem	omensuc 4620	The set of natural numbers is equinumerous to its successor.
⊢ ω ≈ suc ω
Theorem	infensuc 4621	Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88.
⊢ ((A ∈ On ⋀ ω ⊆ A) → A ≈ suc A)
Theorem	unbnnt 4622	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 4530 eliminates its hypothesis by assuming the Axiom of Infinity.
⊢ ((A ⊆ ω ⋀ ∀x ∈ ω ∃y ∈ A x ∈ y) → A ≈ ω)
Theorem	noinfep 4623	Using the Axiom of Regularity in the form zfregfr 4584, show that there are no infinite descending ∈ -chains. Proposition 7.34 of [TakeutiZaring] p. 44.
⊢ (F Fn ω → ∃x ∈ ω ¬ (F ‘suc x) ∈ (F ‘x))
Rank
Syntax	cr1 4624	Extend class definition to include the cumulative hierarchy of sets function.
class R1
Syntax	crnk 4625	Extend class definition to include rank function.
class rank
Definition	df-r1 4626	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 4646). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 4634, r1suc 4635, and r1lim 4636. Theorem r1val1 4641 shows a recursive definition that works for all values, and theorems r1val2 4661 and r1val3 4662 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 = ℘x}, ∅)
Definition	df-rank 4627	Define the rank function. See rankval 4651, rankval2 4653, rankval3 4664, or rankval4 4685 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 4655 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 4660.
⊢ rank = {⟨x, y⟩∣y = ∩{z ∈ On∣x ∈ (R1 ‘suc z)}}
Theorem	trcl 4628	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 4629 for an abbreviated version showing existence.
⊢ A ∈ V    &   ⊢ F = (rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω)    &   ⊢ C = ∪y ∈ ω (F ‘y)    ⇒   ⊢ (A ⊆ C ⋀ Tr C ⋀ ∀x((A ⊆ x ⋀ Tr x) → C ⊆ x))
Theorem	tz9.1 4629	Every set has a transitive closure (smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 4628 for an explicit expression for the transitive closure.
⊢ A ∈ V    ⇒   ⊢ ∃x(A ⊆ x ⋀ Tr x ⋀ ∀y((A ⊆ y ⋀ Tr y) → x ⊆ y))
Theorem	zfregs 4630	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 ≠ ∅ → ∃x ∈ A (x ∩ A) = ∅)
Theorem	setind 4631	Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21.
⊢ (∀x(x ⊆ A → x ∈ A) → A = V)
Theorem	setind2 4632	Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996).
⊢ (℘A ⊆ A → A = V)
Theorem	r1fnon 4633	The cumulative hierarchy of sets function is a function on the class of ordinal numbers.
⊢ R1 Fn On
Theorem	r10 4634	Value of the cumulative hierarchy of sets function at ∅. Part of Definition 9.9 of [TakeutiZaring] p. 76.
⊢ (R1 ‘∅) = ∅
Theorem	r1suc 4635	Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76.
⊢ (A ∈ On → (R1 ‘suc A) = ℘(R1 ‘A))
Theorem	r1lim 4636	Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76.
⊢ ((A ∈ B ⋀ Lim A) → (R1 ‘A) = ∪x ∈ A (R1 ‘x))
Theorem	r1tr 4637	The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202.
⊢ Tr (R1 ‘A)
Theorem	r1ord 4638	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77.
⊢ (B ∈ On → (A ∈ B → (R1 ‘A) ∈ (R1 ‘B)))
Theorem	r1ord2 4639	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77.
⊢ (B ∈ On → (A ∈ B → (R1 ‘A) ⊆ (R1 ‘B)))
Theorem	r1ord3 4640	Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478.
⊢ ((A ∈ On ⋀ B ∈ On) → (A ⊆ B → (R1 ‘A) ⊆ (R1 ‘B)))
Theorem	r1val1 4641	The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202.
⊢ (A ∈ On → (R1 ‘A) = ∪x ∈ A ℘(R1 ‘x))
Theorem	tz9.12lem1 4642	Lemma for tz9.12 4645.
Theorem	tz9.12lem2 4643	Lemma for tz9.12 4645.
Theorem	tz9.12lem3 4644	Lemma for tz9.12 4645.
Theorem	tz9.12 4645	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 4642 through tz9.12lem3 4644.
⊢ A ∈ V    ⇒   ⊢ (∀x ∈ A ∃y ∈ On x ∈ (R1 ‘y) → ∃y ∈ On A ∈ (R1 ‘y))
Theorem	tz9.13 4646	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 ∈ V    ⇒   ⊢ ∃x ∈ On A ∈ (R1 ‘x)
Theorem	tz9.13g 4647	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 4646 expresses the class existence requirement as an antecedent.
⊢ (A ∈ B → ∃x ∈ On A ∈ (R1 ‘x))
Theorem	rankwflem 4648	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 4647 is useful in proofs of theorems about the rank function.
⊢ (A ∈ B → ∃x ∈ On A ∈ (R1 ‘suc x))
Theorem	jech9.3 4649	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.
⊢ ∪x ∈ On (R1 ‘x) = V
Theorem	unir1 4650	The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of [Mendelson] p. 281.
⊢ ∪(R1 “ On) = V
Theorem	rankval 4651	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition).
⊢ A ∈ V    ⇒   ⊢ (rank ‘A) = ∩{x ∈ On∣A ∈ (R1 ‘suc x)}
Theorem	rankvalg 4652	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 4651 expresses the class existence requirement as an antecedent instead of a hypothesis.
⊢ (A ∈ B → (rank ‘A) = ∩{x ∈ On∣A ∈ (R1 ‘suc x)})
Theorem	rankval2 4653	Value of an alternate definition of the rank function. Definition of [BellMachover] p. 478.
⊢ (A ∈ B → (rank ‘A) = ∩{x ∈ On∣A ⊆ (R1 ‘x)})
Theorem	rankon 4654	The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79.
⊢ (rank ‘A) ∈ On
Theorem	rankid 4655	Identity law for the rank function.
⊢ A ∈ V    ⇒   ⊢ A ∈ (R1 ‘suc (rank ‘A))
Theorem	rankr1lem 4656	Lemma for rankr1 4657.
Theorem	rankr1 4657	A relationship between the rank function and the cumulative hierarchy of sets function R1. Proposition 9.15(2) of [TakeutiZaring] p. 79.
⊢ A ∈ V    ⇒   ⊢ (B = (rank ‘A) ↔ (¬ A ∈ (R1 ‘B) ⋀ A ∈ (R1 ‘suc B)))
Theorem	rankr1g 4658	A relationship between the rank function and the cumulative hierarchy of sets function R1. Proposition 9.15(2) of [TakeutiZaring] p. 79.
⊢ (A ∈ C → (B = (rank ‘A) ↔ (¬ A ∈ (R1 ‘B) ⋀ A ∈ (R1 ‘suc B))))
Theorem	ssrankr1 4659	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 ∈ V    ⇒   ⊢ (B ∈ On → (B ⊆ (rank ‘A) ↔ ¬ A ∈ (R1 ‘B)))
Theorem	rankr1a 4660	A relationship between rank and R1, clearly equivalent to ssrankr1 4659 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 4682 for the subset verion. (Contributed by Raph Levien, 29-May-2004.)
⊢ A ∈ V    ⇒   ⊢ (B ∈ On → (A ∈ (R1 ‘B) ↔ (rank ‘A) ∈ B))
Theorem	r1val2 4661	The value of the cumulative hierarchy of sets function expressed in terms of rank. Definition 15.19 of [Monk1] p. 113.
⊢ (A ∈ On → (R1 ‘A) = {x∣(rank ‘x) ∈ A})
Theorem	r1val3 4662	The value of the cumulative hierarchy of sets function expressed in terms of rank. Theorem 15.18 of [Monk1] p. 113.
⊢ (A ∈ On → (R1 ‘A) = ∪x ∈ A ℘{y∣(rank ‘y) ∈ x})
Theorem	rankel 4663	The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79.
⊢ B ∈ V    ⇒   ⊢ (A ∈ B → (rank ‘A) ∈ (rank ‘B))
Theorem	rankval3 4664	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 ∈ V    ⇒   ⊢ (rank ‘A) = ∩{x ∈ On∣∀y ∈ A (rank ‘y) ∈ x}
Theorem	bndrank 4665	Any class whose elements have bounded rank is a set. Proposition 9.19 of [TakeutiZaring] p. 80.
⊢ (∃x ∈ On ∀y ∈ A (rank ‘y) ⊆ x → A ∈ V)
Theorem	unbndrank 4666	The elements of a proper class have unbounded rank. Exercise 2 of [TakeutiZaring] p. 80.
⊢ (¬ A ∈ V → ∀x ∈ On ∃y ∈ A x ∈ (rank ‘y))
Theorem	rankpw 4667	The rank of a power set. Part of Exercise 30 of [Enderton] p. 207.
⊢ A ∈ V    ⇒   ⊢ (rank ‘℘A) = suc (rank ‘A)
Theorem	ranklim 4668	The rank of a set belongs to a limit ordinal iff the rank of its power set does.
⊢ (Lim B → ((rank ‘A) ∈ B ↔ (rank ‘℘A) ∈ B))
Theorem	r1pw 4669	A stronger property of R1 than rankpw 4667. 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 ℘A is in the cumulative hierarchy of the successor. (Contributed by Raph Levien, 29-May-2004.)
⊢ (B ∈ On → (A ∈ (R1 ‘B) ↔ ℘A ∈ (R1 ‘suc B)))
Theorem	r1pwcl 4670	The cumulative hierarchy of a limit ordinal is closed under power set. (Contributed by Raph Levien, 29-May-2004.)
⊢ (Lim B → (A ∈ (R1 ‘B) ↔ ℘A ∈ (R1 ‘B)))
Theorem	rankss 4671	The subset relation is inherited by the rank function. Exercise 1 of [TakeutiZaring] p. 80.
⊢ B ∈ V    ⇒   ⊢ (A ⊆ B → (rank ‘A) ⊆ (rank ‘B))
Theorem	ranksn 4672	The rank of a singleton. Theorem 15.17(v) of [Monk1] p. 112.
⊢ A ∈ V    ⇒   ⊢ (rank ‘{A}) = suc (rank ‘A)
Theorem	rankuni2 4673	The rank of a union. Part of Theorem 15.17(iv) of [Monk1] p. 112.
⊢ A ∈ V    ⇒   ⊢ (rank ‘∪A) = ∪x ∈ A (rank ‘x)
Theorem	rankun 4674	The rank of the union of two sets. Theorem 15.17(iii) of [Monk1] p. 112.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (rank ‘(A ∪ B)) = ((rank ‘A) ∪ (rank ‘B))
Theorem	rankpr 4675	The rank of an unordered pair. Part of Exercise 30 of [Enderton] p. 207.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (rank ‘{A, B}) = suc ((rank ‘A) ∪ (rank ‘B))
Theorem	rankop 4676	The rank of an ordered pair. Part of Exercise 4 of [Kunen] p. 107.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (rank ‘⟨A, B⟩) = suc suc ((rank ‘A) ∪ (rank ‘B))
Theorem	r1rankid 4677	Any set is a subset of the hierarchy of its rank.
⊢ (A ∈ B → A ⊆ (R1 ‘(rank ‘A)))
Theorem	rankonid 4678	The rank of an ordinal number is itself. Proposition 9.18 of [TakeutiZaring] p. 79 and its converse.
⊢ (A ∈ On ↔ (rank ‘A) = A)
Theorem	rankeq0 4679	A set is empty iff its rank is empty.
⊢ A ∈ V    ⇒   ⊢ (A = ∅ ↔ (rank ‘A) = ∅)
Theorem	rankr1id 4680	The rank of the hierarchy of an ordinal number is itself.
⊢ (A ∈ On ↔ (rank ‘(R1 ‘A)) = A)
Theorem	rankuni 4681	The rank of a union. Part of Exercise 4 of [Kunen] p. 107.
⊢ (rank ‘∪A) = ∪(rank ‘A)
Theorem	rankr1b 4682	A relationship between rank and R1. See rankr1a 4660 for the membership version.
⊢ A ∈ V    ⇒   ⊢ (B ∈ On → (A ⊆ (R1 ‘B) ↔ (rank ‘A) ⊆ B))
Theorem	ranksuc 4683	The rank of a successor.
⊢ A ∈ V    ⇒   ⊢ (rank ‘suc A) = suc (rank ‘A)
Theorem	rankuniss 4684	Upper bound of the rank of a union. Part of Exercise 30 of [Enderton] p. 207.
⊢ A ∈ V    ⇒   ⊢ (rank ‘∪A) ⊆ (rank ‘A)
Theorem	rankval4 4685	The rank of a set is the supremum of the successors of the ranks of its members. Exercise 9.1 of [Jech] p. 72. Also a special case of Theorem 7V(b) of [Enderton] p. 204.
⊢ A ∈ V    ⇒   ⊢ (rank ‘A) = ∪x ∈ A suc (rank ‘x)
Theorem	rankbnd 4686	The rank of a set is bounded by a bound for the successor of its members.
⊢ A ∈ V    ⇒   ⊢ (∀x ∈ A suc (rank ‘x) ⊆ B ↔ (rank ‘A) ⊆ B)
Theorem	rankbnd2 4687	The rank of a set is bounded by the successor of a bound for its members.
⊢ A ∈ V    ⇒   ⊢ (B ∈ On → (∀x ∈ A (rank ‘x) ⊆ B ↔ (rank ‘A) ⊆ suc B))
Theorem	rankc1 4688	A relationship that can be used for computation of rank.
⊢ A ∈ V    ⇒   ⊢ (∀x ∈ A (rank ‘x) ∈ (rank ‘∪A) ↔ (rank ‘A) = (rank ‘∪A))
Theorem	rankc2 4689	A relationship that can be used for computation of rank.
⊢ A ∈ V    ⇒   ⊢ (∃x ∈ A (rank ‘x) = (rank ‘∪A) → (rank ‘A) = suc (rank ‘∪A))
Theorem	rankelun 4690	Rank membership is inherited by union.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ (((rank ‘A) ∈ (rank ‘C) ⋀ (rank ‘B) ∈ (rank ‘D)) → (rank ‘(A ∪ B)) ∈ (rank ‘(C ∪ D)))
Theorem	rankelpr 4691	Rank membership is inherited by unordered pairs.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ (((rank ‘A) ∈ (rank ‘C) ⋀ (rank ‘B) ∈ (rank ‘D)) → (rank ‘{A, B}) ∈ (rank ‘{C, D}))
Theorem	rankelop 4692	Rank membership is inherited by ordered pairs.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ (((rank ‘A) ∈ (rank ‘C) ⋀ (rank ‘B) ∈ (rank ‘D)) → (rank ‘⟨A, B⟩) ∈ (rank ‘⟨C, D⟩))
Theorem	rankxpl 4693	A lower bound on the rank of a cross product.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((A × B) ≠ ∅ → (rank ‘(A ∪ B)) ⊆ (rank ‘(A × B)))
Theorem	rankxpu 4694	An upper bound on the rank of a cross product.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (rank ‘(A × B)) ⊆ suc suc (rank ‘(A ∪ B))
Theorem	rankxplim 4695	The rank of a cross product when the rank of the union of its arguments is a limit ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxpsuc 4698 for the successor case.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((Lim (rank ‘(A ∪ B)) ⋀ (A × B) ≠ ∅) → (rank ‘(A × B)) = (rank ‘(A ∪ B)))
Theorem	rankxplim2 4696	If the rank of a cross product is a limit ordinal, so is the rank of the union of its arguments.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (Lim (rank ‘(A × B)) → Lim (rank ‘(A ∪ B)))
Theorem	rankxplim3 4697	The rank of a cross product is a limit ordinal iff its union is.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (Lim (rank ‘(A × B)) ↔ Lim ∪(rank ‘(A × B)))
Theorem	rankxpsuc 4698	The rank of a cross product when the rank of the union of its arguments is a successor ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxplim 4695 for the limit ordinal case.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (((rank ‘(A ∪ B)) = suc C ⋀ (A × B) ≠ ∅) → (rank ‘(A × B)) = suc suc (rank ‘(A ∪ B)))
Scott's trick; collection principle; Hilbert's epsilon
Theorem	scottex 4699	Scott's trick collects all sets that have a certain property and are of smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of [Jech] p. 72, is a set.
⊢ {x ∈ A∣∀y ∈ A (rank ‘x) ⊆ (rank ‘y)} ∈ V
Theorem	scott0 4700	Scott's trick collects all sets that have a certain property and are of smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of [Jech] p. 72, contains at least one representative with the property, if there is one. In other words, the collection is empty iff no set has the property (i.e. A is empty).
⊢ (A = ∅ ↔ {x ∈ A∣∀y ∈ A (rank ‘x) ⊆ (rank ‘y)} = ∅)