Home | Metamath
Proof Explorer Theorem List (p. 73 of 313) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21423) |
Hilbert Space Explorer
(21424-22946) |
Users' Mathboxes
(22947-31284) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | card2on 7201* | Proof that the alternate definition cardval2 7557 is always a set, and indeed is an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.) |
Theorem | card2inf 7202* | The definition cardval2 7557 has the curious property that for non-numerable sets (for which ndmfv 5451 yields ), it still evaluates to a non-empty set, and indeed it contains . (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 27-Apr-2015.) |
Syntax | char 7203 | Class symbol for the Hartogs/cardinal successor function. |
har | ||
Syntax | cwdom 7204 | Class symbol for the weak dominance relation. |
^{*} | ||
Definition | df-har 7205* |
Define the Hartogs function , which maps all sets to the smallest
ordinal that cannot be injected into the given set. In the important
special case where is an ordinal, this is the cardinal successor
operation.
Traditionally, the Hartogs number of a set is written and the cardinal successor ; we use functional notation for this, and cannot use the aleph symbol because it is taken for the enumerating function of the infinite initial ordinals df-aleph 7506. Some authors define the Hartogs number of a set to be the least *infinite* ordinal which does not inject into it, thus causing the range to consist only of alephs. We use the simpler definition where the value can be any successor cardinal. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
har | ||
Definition | df-wdom 7206* | A set is weakly dominated by a "larger" set iff the "larger" set can be mapped onto the "smaller" set or the smaller set is empty; equivalently if the smaller set can be placed into bijection with some partition of the larger set. When choice is assumed (as fodom 8082), this concides with the 1-1 defition df-dom 6798; however, it is not known whether this is a choice-equivalent or a strictly weaker form. Some discussion of this question can be found at http://boolesrings.org/asafk/2014/on-the-partition-principle/. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
^{*} | ||
Theorem | harf 7207 | Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
har | ||
Theorem | harcl 7208 | Closure of the Hartogs function in the ordinals. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
har | ||
Theorem | harval 7209* | Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
har | ||
Theorem | elharval 7210 | The Hartogs number of a set is greater than all ordinals which inject into it. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
har | ||
Theorem | harndom 7211 | The Hartogs number of a set does not inject into that set. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
har | ||
Theorem | harword 7212 | Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
har har | ||
Theorem | relwdom 7213 | Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
^{*} | ||
Theorem | brwdom 7214* | Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015.) |
^{*} | ||
Theorem | brwdomi 7215* | Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015.) |
^{*} | ||
Theorem | brwdomn0 7216* | Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
^{*} | ||
Theorem | 0wdom 7217 | Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
^{*} | ||
Theorem | fowdom 7218 | An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
^{*} | ||
Theorem | wdomref 7219 | Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
^{*} | ||
Theorem | brwdom2 7220* | Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
^{*} | ||
Theorem | domwdom 7221 | Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
^{*} | ||
Theorem | wdomtr 7222 | Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
^{*} ^{*} ^{*} | ||
Theorem | wdomen1 7223 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
^{*} ^{*} | ||
Theorem | wdomen2 7224 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
^{*} ^{*} | ||
Theorem | wdompwdom 7225 | Weak dominance strengthens to usual dominance on the power sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
^{*} | ||
Theorem | canthwdom 7226 | Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 6947, equivalent to canth 6225). (Contributed by Mario Carneiro, 15-May-2015.) |
^{*} | ||
Theorem | wdom2d 7227* | Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep 4071). (Contributed by Stefan O'Rear, 13-Feb-2015.) |
^{*} | ||
Theorem | wdomd 7228* | Deduce weak dominance from an implicit onto function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
^{*} | ||
Theorem | brwdom3 7229* | Condition for weak dominance with a condition reminiscent of wdomd 7228. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
^{*} | ||
Theorem | brwdom3i 7230* | Weak dominance implies existance of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
^{*} | ||
Theorem | unwdomg 7231 | Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
^{*} ^{*} ^{*} | ||
Theorem | xpwdomg 7232 | Weak dominance of a cross product. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
^{*} ^{*} ^{*} | ||
Theorem | wdomima2g 7233 | A set is weakly dominant over its image under any function. This version of wdomimag 7234 is stated so as to avoid ax-rep 4071. (Contributed by Mario Carneiro, 25-Jun-2015.) |
^{*} | ||
Theorem | wdomimag 7234 | A set is weakly dominant over its image under any function. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
^{*} | ||
Theorem | unxpwdom2 7235 | Lemma for unxpwdom 7236. (Contributed by Mario Carneiro, 15-May-2015.) |
^{*} | ||
Theorem | unxpwdom 7236 | If a cross product is dominated by a union, then the base set is either weakly dominated by one factor of the union or dominated by the other. Extracted from Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.) |
^{*} | ||
Theorem | harwdom 7237 | The Hartogs function is weakly dominated by . This follows from a more precise analysis of the bound used in hartogs 7192 to prove that har is a set. (Contributed by Mario Carneiro, 15-May-2015.) |
har ^{*} | ||
Theorem | ixpiunwdom 7238* | Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg 6779 this shows that and have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015.) |
^{*} | ||
Axiom | ax-reg 7239* | 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 7242) 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 7244). A stronger version that works for proper classes is proved as zfregs 7347. (Contributed by NM, 14-Aug-1993.) |
Theorem | axreg2 7240* | Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003.) |
Theorem | zfregcl 7241* | The Axiom of Regularity with class variables. (Contributed by NM, 5-Aug-1994.) |
Theorem | zfreg 7242* | 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 be a set, that can be proved with more difficulty (see zfregs 7347). (Contributed by NM, 26-Nov-1995.) |
Theorem | zfreg2 7243* | The Axiom of Regularity using abbreviations. This form with the intersection arguments commuted (compared to zfreg 7242) is formally more convenient for us in some cases. Axiom Reg of [BellMachover] p. 480. (Contributed by NM, 17-Sep-2003.) |
Theorem | elirrv 7244 | 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 7249 and efrirr 4311, but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993.) |
Theorem | elirr 7245 | No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | sucprcreg 7246 | A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity). (Contributed by NM, 9-Jul-2004.) |
Theorem | ruv 7247 | The Russell class is equal to the universe . Exercise 5 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 4-Oct-2008.) |
Theorem | ruALT 7248 | Alternate proof of Russell's Paradox ru 2934, simplified using (indirectly) the Axiom of Regularity ax-reg 7239. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) |
Theorem | zfregfr 7249 | The epsilon relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.) |
Theorem | en2lp 7250 | No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206. (Contributed by NM, 16-Oct-1996.) (Revised by Mario Carneiro, 25-Jun-2015.) |
Theorem | preleq 7251 | Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) |
Theorem | opthreg 7252 | Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 7239 (via the preleq 7251 step). See df-op 3590 for a description of other ordered pair representations. Exercise 34 of [Enderton] p. 207. (Contributed by NM, 16-Oct-1996.) |
Theorem | suc11reg 7253 | The successor operation behaves like a one-to-one function (assuming the Axiom of Regularity). Exercise 35 of [Enderton] p. 208 and its converse. (Contributed by NM, 25-Oct-2003.) |
Theorem | dford2 7254* | Assuming ax-reg 7239, an ordinal is a transitive class on which inclusion satisfies trichotomy. (Contributed by Scott Fenton, 27-Oct-2010.) |
Theorem | inf0 7255* | Our Axiom of Infinity derived from existence of omega. The proof shows that the especially contrived class " " exists, is a subset of its union, and contains a given set (and thus is non-empty). Thus it provides an example demonstrating that a set exists with the necessary properties demanded by ax-inf 7272. (Contributed by NM, 15-Oct-1996.) |
Theorem | inf1 7256 | Variation of Axiom of Infinity (using zfinf 7273 as a hypothesis). Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 14-Oct-1996.) (Revised by David Abernethy, 1-Oct-2013.) |
Theorem | inf2 7257* | Variation of Axiom of Infinity. There exists a non-empty set that is a subset of its union (using zfinf 7273 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 28-Oct-1996.) |
Theorem | inf3lema 7258* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. (Contributed by NM, 28-Oct-1996.) |
Theorem | inf3lemb 7259* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. (Contributed by NM, 28-Oct-1996.) |
Theorem | inf3lemc 7260* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. (Contributed by NM, 28-Oct-1996.) |
Theorem | inf3lemd 7261* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. (Contributed by NM, 28-Oct-1996.) |
Theorem | inf3lem1 7262* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. (Contributed by NM, 28-Oct-1996.) |
Theorem | inf3lem2 7263* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. (Contributed by NM, 28-Oct-1996.) |
Theorem | inf3lem3 7264* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 7242. (Contributed by NM, 29-Oct-1996.) |
Theorem | inf3lem4 7265* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. (Contributed by NM, 29-Oct-1996.) |
Theorem | inf3lem5 7266* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. (Contributed by NM, 29-Oct-1996.) |
Theorem | inf3lem6 7267* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. (Contributed by NM, 29-Oct-1996.) |
Theorem | inf3lem7 7268* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 7269 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex 5650. (Contributed by NM, 29-Oct-1996.) (Proof shortened by Mario Carneiro, 19-Jan-2013.) |
Theorem | inf3 7269 |
Our Axiom of Infinity ax-inf 7272 implies the standard Axiom of Infinity.
The hypothesis is a variant of our Axiom of Infinity provided by
inf2 7257, 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 7274 and zfinf2 7276.) The main proof is provided by
inf3lema 7258 through inf3lem7 7268, and this final piece eliminates the
auxiliary hypothesis of inf3lem7 7268. 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 7259.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 7260.) 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 7262.) 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 7263.) 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 7264.) 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 7265.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 7266.) 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 7267.) 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 7268.) Q.E.D.(Contributed by NM, 29-Oct-1996.) |
Theorem | infeq5i 7270 | Half of infeq5 7271. (Contributed by Mario Carneiro, 16-Nov-2014.) |
Theorem | infeq5 7271 | 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 7277.) 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. (Contributed by NM, 23-Mar-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
Axiom | ax-inf 7272* |
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 , an infinite set
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 7256
and
inf2 7257). More standard versions, which essentially
state that there
exists a set containing all the natural numbers, are shown as zfinf2 7276
and omex 7277 and are based on the (nontrivial) proof of inf3 7269.
Our
version has the advantage that when expanded to primitives, it has fewer
symbols than the standard version ax-inf2 7275. Theorem inf0 7255
shows the
reverse derivation of our axiom from a standard one. Theorem inf5 7279
shows a very short way to state this axiom.
The standard version of Infinity ax-inf2 7275 requires this axiom along with Regularity ax-reg 7239 for its derivation (as theorem axinf2 7274 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 7275 instead of this one. The derivation of this axiom from ax-inf2 7275 is shown by theorem axinf 7278. (Contributed by NM, 16-Aug-1993.) |
Theorem | zfinf 7273* | Axiom of Infinity expressed with fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
Theorem | axinf2 7274* |
A standard version of Axiom of Infinity, expanded to primitives, derived
from our version of Infinity ax-inf 7272 and Regularity ax-reg 7239.
This theorem should not be referenced in any proof. Instead, use ax-inf2 7275 below so that the ordinary uses of Regularity can be more easily identified. (New usage is discouraged.) (Contributed by NM, 3-Nov-1996.) |
Axiom | ax-inf2 7275* | 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 7276 shows it converted to abbreviations. This axiom was derived as theorem axinf2 7274 above, using our version of Infinity ax-inf 7272 and the Axiom of Regularity ax-reg 7239. We will reference ax-inf2 7275 instead of axinf2 7274 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 7272 from ax-inf2 7275 is shown by theorem axinf 7278. (Contributed by NM, 30-Aug-1993.) |
Theorem | zfinf2 7276* | A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 7275 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993.) |
Theorem | omex 7277 |
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 7255.
A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial ; this would lead to by omon 4604 and (the universe of all sets) by fineqv 7011. 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 4612 through peano5 4616 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
Theorem | axinf 7278* | The first version of the Axiom of Infinity ax-inf 7272 proved from the second version ax-inf2 7275. Note that we didn't use ax-reg 7239, unlike the other direction axinf2 7274. (Contributed by NM, 24-Apr-2009.) |
Theorem | inf5 7279 | The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see theorem infeq5 7271). This provides us with a very compact way to express of the Axiom of Infinity using only elementary symbols. (Contributed by NM, 3-Jun-2005.) |
Theorem | omelon 7280 | Omega is an ordinal number. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.) |
Theorem | dfom3 7281* | 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. (Contributed by NM, 6-Aug-1994.) |
Theorem | elom3 7282* | A simplification of elom 4596 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.) |
Theorem | dfom4 7283* | A simplification of df-om 4594 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.) |
Theorem | dfom5 7284 | is the smallest limit ordinal and can be defined as such (although the Axiom of Infinity is needed to ensure that at least one limit ordinal exists). (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 2-Feb-2013.) |
Theorem | oancom 7285 | Ordinal addition is not commutative. This theorem shows a counterexample. Remark in [TakeutiZaring] p. 60. (Contributed by NM, 10-Dec-2004.) |
Theorem | isfinite 7286 | A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of [Suppes] p. 151. The Axiom of Infinity is used for the forward implication. (Contributed by FL, 16-Apr-2011.) |
Theorem | nnsdom 7287 | A natural number is strictly dominated by the set of natural numbers. Example 3 of [Enderton] p. 146. (Contributed by NM, 28-Oct-2003.) |
Theorem | omenps 7288 | Omega is equinumerous to a proper subset of itself. Example 13.2(4) of [Eisenberg] p. 216. (Contributed by NM, 30-Jul-2003.) |
Theorem | omensuc 7289 | The set of natural numbers is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
Theorem | infdifsn 7290 | Removing a singleton from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Mario Carneiro, 16-May-2015.) |
Theorem | infdiffi 7291 | Removing a finite set from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015.) |
Theorem | unbnn3 7292* | Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 7046 eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005.) |
Theorem | noinfep 7293* | Using the Axiom of Regularity in the form zfregfr 7249, show that there are no infinite descending -chains. Proposition 7.34 of [TakeutiZaring] p. 44. (Contributed by NM, 26-Jan-2006.) (Revised by Mario Carneiro, 22-Mar-2013.) |
Theorem | noinfepOLD 7294* | Using the Axiom of Regularity in the form zfregfr 7249, show that there are no infinite descending -chains. Proposition 7.34 of [TakeutiZaring] p. 44. (Contributed by NM, 26-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Syntax | ccnf 7295 | Extend class notation with the Cantor normal form function. |
CNF | ||
Definition | df-cnf 7296* | Define the Cantor normal form function, which takes as input a finitely supported function from to and outputs the corresponding member of the ordinal exponential . The content of the original Cantor Normal Form theorem is that for this function is a bijection onto for any ordinal (or, since the function restricts naturally to different ordinals, the statement that the composite function is a bijection to ). More can be said about the function, however, and in particular it is an order isomorphism for a certain easily defined well-ordering of the finitely supported functions, which gives an alternate definition cantnffval2 7330 of this function in terms of df-oi 7158. (Contributed by Mario Carneiro, 25-May-2015.) |
CNF OrdIso seq_{𝜔} | ||
Theorem | cantnffval 7297* | The value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015.) |
CNF OrdIso seq_{𝜔} | ||
Theorem | cantnfdm 7298* | The domain of the Cantor normal form function (in later lemmas we will use CNF to abbreviate "the set of finitely supported functions from to "). (Contributed by Mario Carneiro, 25-May-2015.) |
CNF | ||
Theorem | cantnfvalf 7299* | Lemma for cantnf 7328. The function appearing in cantnfval 7302 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.) |
seq_{𝜔} | ||
Theorem | cantnfs 7300 | Elementhood in the set of finitely supported functions from to . (Contributed by Mario Carneiro, 25-May-2015.) |
CNF |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |