mmtheorems49 - 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-10691

Statement List for Metamath Proof Explorer - 4801-4900 - Page 49 of 107

Type	Label	Description
Statement
Definition	df-cf 4801	Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 4889 for its value and a description.
|- cf = {<.x, y>. | (x e. On /\ y = |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))})}
Theorem	oncardval 4802	The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 4809, this theorem does not require the Axiom of Choice.
|- (A e. On -> (card` A) = |^|{x e. On | x ~~ A})
Theorem	oncardon 4803	The cardinal number of an ordinal number is an ordinal number. Unlike cardon 4810, this theorem does not require the Axiom of Choice.
|- (A e. On -> (card` A) e. On)
Theorem	oncardid 4804	Any ordinal number is equinumerous to its cardinal number. Unlike cardid 4811, this theorem does not require the Axiom of Choice.
|- (A e. On -> (card` A) ~~ A)
Theorem	cardonle 4805	The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85.
|- (A e. On -> (card` A) (_ A)
Theorem	card0 4806	The cardinality of the empty set is the empty set.
|- (card` (/)) = (/)
Theorem	cardnn 4807	The cardinality of a natural number is the number. Corollary 10.23 of [TakeutiZaring] p. 90.
|- (A e. om -> (card` A) = A)
Theorem	cardom 4808	The set of natural numbers is a cardinal number. Theorem 18.11 of [Monk1] p. 133.
|- (card` om) = om
Theorem	cardval 4809	The value of the cardinal number function. Definition 10.4 of [TakeutiZaring] p. 85. See cardval2 4838 for a simpler version of its value.
|- (card` A) = |^|{x e. On | x ~~ A}
Theorem	cardon 4810	The cardinal number of a set is an ordinal number. Proposition 10.6(1) of [TakeutiZaring] p. 85. Unlike Takeuti/Zaring's proposition, we need the Axiom of Choice (in cardval 4809) because of our slightly different definition of of cardinal number.
|- (card` A) e. On
Theorem	cardid 4811	Any set is equinumerous to its cardinal number. Proposition 10.5 of [TakeutiZaring] p. 85.
|- (card` A) ~~ A
Theorem	oncard 4812	A set is a cardinal number iff it equals its own cardinal number. Proposition 10.9 of [TakeutiZaring] p. 85.
|- (E.x A = (card` x) <-> A = (card` A))
Theorem	cardne 4813	No member of a cardinal number of a set is equinumerous to the set. Proposition 10.6(2) of [TakeutiZaring] p. 85.
|- (A e. (card` B) -> -. A ~~ B)
Theorem	carden 4814	Two sets are equinumerous iff their cardinal numbers are equal. This important theorem expresses the essential concept behind "cardinality" or "size." This theorem appears as Proposition 10.10 of [TakeutiZaring] p. 85, Theorem 7P of [Enderton] p. 197, and Theorem 9 of [Suppes] p. 242 (among others). The Axiom of Choice is required for its proof. The theory of cardinality can also be developed without AC by introducing "card" as a primitive notion and stating this theorem as an axiom, as is done with the axiom for cardinal numbers in [Suppes] p. 111. Finally, if we allow the Axiom of Regularity, we can avoid AC by defining the cardinal number of a set as the set of all sets equinumerous to it and having least possible rank (see karden 4709).
|- ((A e. C /\ B e. D) -> ((card` A) = (card` B) <-> A ~~ B))
Theorem	cardeq0 4815	Only the empty set has cardinality zero.
|- (A e. B -> ((card` A) = (/) <-> A = (/)))
Theorem	card1 4816	A set has cardinality one iff it is a singleton.
|- ((card` A) = 1o <-> E.x A = {x})
Theorem	cardsn 4817	A singleton has cardinality one.
|- (A e. B -> (card` {A}) = 1o)
Theorem	carddomi 4818	Two sets have the dominance relationship if their cardinalities have the subset relationship.
|- (A e. C -> ((card` A) (_ (card` B) -> A ~<_ B))
Theorem	carddom 4819	Two sets have the dominance relationship iff their cardinalities have the subset relationship. Equation i of [Quine] p. 232.
|- ((A e. C /\ B e. D) -> ((card` A) (_ (card` B) <-> A ~<_ B))
Theorem	cardsdom 4820	Two sets have the strict dominance relationship iff their cardinalities have the membership relationship. Corollary 19.7(2) of [Eisenberg] p. 310.
|- ((A e. C /\ B e. D) -> ((card` A) e. (card` B) <-> A ~< B))
Theorem	domtri 4821	Trichotomy law for dominance and strict dominance. This theorem is equivalent to the Axiom of Choice.
|- ((A e. C /\ B e. D) -> (A ~<_ B <-> -. B ~< A))
Theorem	entri 4822	Trichotomy of equinumerosity and strict dominance. This theorem is equivalent to the Axiom of Choice. Theorem 8 of [Suppes] p. 242.
|- ((A e. C /\ B e. D) -> (A ~< B \/ A ~~ B \/ B ~< A))
Theorem	entri2 4823	Trichotomy of dominance and strict dominance.
|- ((A e. C /\ B e. D) -> (A ~<_ B \/ B ~< A))
Theorem	entri3 4824	Trichotomy of dominance. This theorem is equivalent to the Axiom of Choice. Part of Proposition 4.42(d) of [Mendelson] p. 275.
|- ((A e. C /\ B e. D) -> (A ~<_ B \/ B ~<_ A))
Theorem	sucdom 4825	Strict dominance of a set over a natural number is the same as dominance over its successor. The proof uses AC and Infinity. It is unclear if a proof without using these is possible, unlike the weaker versions omsucdom 4511, sucdomi 4512, and finsucdom 4515.
|- ((A e. om /\ B e. C) -> (A ~< B <-> suc A ~<_ B))
Theorem	unxpdomlem 4826	Lemma for unxpdom 4827.
Theorem	unxpdom 4827	Cross product dominates union for sets with cardinality greater than 1. Proposition 10.36 of [TakeutiZaring] p. 93.
|- ((1o ~< A /\ 1o ~< B) -> (A u. B) ~<_ (A X. B))
Theorem	unxpdom2 4828	Corollary of unxpdom 4827.
|- A e. V   &   |- B e. V   =>   |- ((1o ~< A /\ B ~<_ A) -> (A u. B) ~<_ (A X. A))
Theorem	sucxpdom 4829	Cross product dominates successor for set with cardinality greater than 1. Proposition 10.38 of [TakeutiZaring] p. 93 (but generalized to arbitrary sets, not just ordinals, with a proof using AC).
|- (1o ~< A -> suc A ~<_ (A X. A))
Theorem	sdomel 4830	Strict dominance implies ordinal membership.
|- ((A e. On /\ B e. On) -> (A ~< B -> A e. B))
Theorem	sdomsdomcard 4831	A set strictly dominates iff its cardinal strictly dominates.
|- (A ~< B <-> A ~< (card` B))
Theorem	cardidm 4832	The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85.
|- (card` (card` A)) = (card` A)
Theorem	canth3 4833	Cantor's theorem in terms of cardinals. This theorem tells us that no matter how large a cardinal number is, there is a still larger cardinal number. Theorem 18.12 of [Monk1] p. 133.
|- (A e. B -> (card` A) e. (card` P~A))
Theorem	cardlim 4834	An infinite cardinal is a limit ordinal. Equivalent to Exercise 4 of [TakeutiZaring] p. 91.
|- (om (_ (card` A) <-> Lim (card` A))
Theorem	cardsdomel 4835	A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93 (use cardsdom 4820 to obtain the exact proposition from this one).
|- (A e. On -> (A ~< B <-> A e. (card` B)))
Theorem	iscard 4836	Two ways to express the property of being a cardinal number.
|- ((card` A) = A <-> (A e. On /\ A.x e. A x ~< A))
Theorem	iscard2 4837	Two ways to express the property of being a cardinal number. Definition 8 of [Suppes] p. 225.
|- ((card` A) = A <-> (A e. On /\ A.x e. On (A ~~ x -> A (_ x)))
Theorem	cardval2 4838	An alternate version of the value of the cardinal number of a set. Compare cardval 4809. This theorem could be used to give us a simpler definition of card in place of df-card 4799. It apparently does not occur in the literature.
|- (card` A) = {x e. On | x ~< A}
Theorem	ondomon 4839	The collection of ordinal numbers dominated by a set is an ordinal number. (In general, not all collections of ordinal numbers are ordinal.) Theorem 56 of [Suppes] p. 227.
|- (A e. B -> {x e. On | x ~<_ A} e. On)
Theorem	ondomcard 4840	The class of ordinal numbers dominated by a set is a cardinal number. Theorem 59 of [Suppes] p. 228.
|- (A e. B -> (card` {x e. On | x ~<_ A}) = {x e. On | x ~<_ A})
Theorem	carduni 4841	The union of a set of cardinals is a cardinal. Theorem 18.14 of [Monk1] p. 133.
|- (A e. B -> (A.x e. A (card` x) = x -> (card` U.A) = U.A))
Theorem	cardiun 4842	The indexed union of a set of cardinals is a cardinal.
|- (A e. C -> (A.x e. A (card` B) = B -> (card` U_x e. A B) = U_x e. A B))
Theorem	cardmin 4843	The smallest ordinal that strictly dominates a set is a cardinal.
|- (A e. B -> (card` |^|{x e. On | A ~< x}) = |^|{x e. On | A ~< x})
Theorem	cardprc 4844	The class of all cardinal numbers is not a set (i.e. is a proper class). Theorem 19.8 of [Eisenberg] p. 310.
|- -. {x | (card` x) = x} e. V
Theorem	alephfnon 4845	The aleph function is a function on the class of ordinal numbers.
|- aleph Fn On
Theorem	aleph0 4846	The first infinite cardinal number, discovered by Georg Cantor in 1873, has the same size as the set of natural numbers om (and under our particular definition is also equal to it). In the literature, the argument of the aleph function is often written as a subscript, and the first aleph is written aleph0. Exercise 3 of [TakeutiZaring] p. 91. Also Definition 12(i) of [Suppes] p. 228. From Kuratowski and Mostowski, Set Theory, p. 95: "Aleph...the first letter in the Hebrew alphabet...is also the first letter of the Hebrew word...(einsoph, meaning infinity), which is a cabbalistic appellation of the deity. The notation is due to Cantor, who was deeply interested in mysticism."
|- (aleph` (/)) = om
Theorem	alephlim 4847	Value of the aleph function at a limit ordinal. Definition 12(iii) of [Suppes] p. 91.
|- ((A e. B /\ Lim A) -> (aleph` A) = U_x e. A (aleph` x))
Theorem	alephon 4848	An aleph is an ordinal number.
|- (aleph` A) e. On
Theorem	alephsuc 4849	Value of the aleph function at a successor ordinal. Definition 12(ii) of [Suppes] p. 91.
|- (A e. On -> (aleph` suc A) = |^|{x e. On | (aleph` A) ~< x})
Theorem	alephcard 4850	Every aleph is a cardinal number. Theorem 65 of [Suppes] p. 229.
|- (card` (aleph` A)) = (aleph` A)
Theorem	alephnbtwn 4851	No cardinal can be sandwiched between an aleph and its successor aleph. Theorem 67 of [Suppes] p. 229.
|- ((card` B) = B -> -. ((aleph` A) e. B /\ B e. (aleph` suc A)))
Theorem	alephnbtwn2 4852	No set has equinumerosity between an aleph and its successor aleph.
|- -. ((aleph` A) ~< B /\ B ~< (aleph` suc A))
Theorem	alephsucpw 4853	The power set of an aleph dominates the successor aleph. (The Generalized Continuum Hypothesis says they are equinumerous.)
|- (aleph` suc A) ~<_ P~(aleph` A)
Theorem	aleph1 4854	The set exponentiation of 2 to the aleph-zero has cardinality of at least aleph-one. (If we were to assume the Continuum Hypothesis, their cardinalities would be the same.)
|- (aleph` 1o) ~<_ (2o ^m (aleph` (/)))
Theorem	alephordlem1 4855	Lemma for alephordi 4857.
Theorem	alephordlem2 4856	Lemma for alephordi 4857.
Theorem	alephordi 4857	Strict ordering property of the aleph function.
|- (B e. On -> (A e. B -> (aleph` A) ~< (aleph` B)))
Theorem	alephord 4858	Ordering property of the aleph function.
|- ((A e. On /\ B e. On) -> (A e. B <-> (aleph` A) ~< (aleph` B)))
Theorem	alephord2 4859	Ordering property of the aleph function. Theorem 8A(a) of [Enderton] p. 213 and its converse.
|- ((A e. On /\ B e. On) -> (A e. B <-> (aleph` A) e. (aleph` B)))
Theorem	alephord2i 4860	Ordering property of the aleph function. Theorem 66 of [Suppes] p. 229.
|- (B e. On -> (A e. B -> (aleph` A) e. (aleph` B)))
Theorem	alephord3 4861	Ordering property of the aleph function.
|- ((A e. On /\ B e. On) -> (A (_ B <-> (aleph` A) (_ (aleph` B)))
Theorem	aleph11 4862	The aleph function is one-to-one.
|- ((A e. On /\ B e. On) -> ((aleph` A) = (aleph` B) <-> A = B))
Theorem	alephsucdom 4863	A set dominated by an aleph is strictly dominated by its successor aleph and vice-versa.
|- (B e. On -> (A ~<_ (aleph` B) <-> A ~< (aleph` suc B)))
Theorem	alephsuc2 4864	An alternate representation of a successor aleph. Using this theorem we could define the aleph function with {z e. On | z ~<_ x} in place of |^|{z e. On | x ~< z} in df-aleph 4800.
|- (A e. On -> (aleph` suc A) = {x e. On | x ~<_ (aleph` A)})
Theorem	alephgeom 4865	Every aleph is greater than or equal to the set of natural numbers.
|- (A e. On <-> om (_ (aleph` A))
Theorem	alephislim 4866	Every aleph is a limit ordinal.
|- (A e. On <-> Lim (aleph` A))
Theorem	alephle 4867	The argument of the aleph function is less than or equal to its value. Exercise 2 of [TakeutiZaring] p. 91. (Later, in alephfp2 4884, we will that equality can sometimes hold.)
|- (A e. On -> A (_ (aleph` A))
Theorem	cardaleph 4868	Given any transfinite cardinal number A, there is exactly one aleph that is equal to it. Here we compute that aleph explicitly.
|- ((om (_ A /\ (card` A) = A) -> A = (aleph` |^|{x e. On | A (_ (aleph