| Metamath Proof Explorer | < Previous Next > | |
| Browser slow? Try the
Unicode version. |
| Color key: | (1-9056) |
(9057-10644) |
(10645-12110) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | sbthbg 4601 | Schroeder-Bernstein Theorem and its converse. |
| Theorem | sbthcl 4602 | Schroeder-Bernstein Theorem in class form. |
| Theorem | dfsdom2 4603 | Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97. |
| Theorem | brsdom2 4604 | Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97. |
| Theorem | sdomnsym 4605 | Strict dominance is not symmetric. Theorem 21(ii) of [Suppes] p. 97. |
| Theorem | domnsym 4606 | Theorem 22(i) of [Suppes] p. 97. |
| Theorem | 0dom 4607 | Any set dominates the empty set. |
| Theorem | dom0 4608 | A set dominated by the empty set is empty. |
| Theorem | 0sdomg 4609 | A set strictly dominates the empty set iff it is not empty. |
| Theorem | 0sdom 4610 | A set strictly dominates the empty set iff it is not empty. |
| Theorem | sdom0 4611 | The empty set does not strictly dominate any set. |
| Theorem | sdomdomtr 4612 | Transitivity of strict dominance and dominance. Theorem 22(iii) of [Suppes] p. 97. |
| Theorem | sdomentr 4613 | Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98. |
| Theorem | ensdomtr 4614 | Transitivity of equinumerosity and strict dominance. |
| Theorem | sdomirr 4615 | Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97. |
| Theorem | sdomex 4616 | Technical lemma for simplifying proofs involving strict dominance. |
| Theorem | sdomtr 4617 | Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97. |
| Theorem | sdomn2lp 4618 | Strict dominance has no 2-cycle loops. |
| Theorem | domsdomtr 4619 | Transitivity of dominance and strict dominance. Theorem 22(ii) of [Suppes] p. 97. |
| Theorem | enen1 4620 | Equality-like theorem for equinumerosity. |
| Theorem | enen2 4621 | Equality-like theorem for equinumerosity. |
| Theorem | domen1 4622 | Equality-like theorem for equinumerosity and dominance. |
| Theorem | domen2 4623 | Equality-like theorem for equinumerosity and dominance. |
| Theorem | sdomen1 4624 | Equality-like theorem for equinumerosity and strict dominance. |
| Theorem | sdomen2 4625 | Equality-like theorem for equinumerosity and strict dominance. |
| Theorem | fodomr 4626 | There exists a mapping from a set onto any (non-empty) set that it dominates. |
| Theorem | canth2 4627 | Cantor's Theorem. No set is equinumerous to its power set. Specifically, any set has a cardinality (size) strictly less than the cardinality of its power set. For example, the cardinality of real numbers is the same as the cardinality of the power set of integers, so real numbers cannot be put into a one-to-one correspondence with integers. Theorem 23 of [Suppes] p. 97. For the function version, see canth 4203. |
| Theorem | canth2g 4628 | Cantor's theorem with the sethood requirement expressed as an antecedent. Theorem 23 of [Suppes] p. 97. |
| Theorem | pwuninel 4629 | The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. |
| Theorem | 2pwuninel 4630 | The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. |
| Theorem | pwne 4631 | No set equals its power set. |
| Theorem | 2pwne 4632 | No set equals the power set of its power set. |
| Theorem | xpen 4633 | Equinumerosity law for cross product. Proposition 4.22(b) of [Mendelson] p. 254. |
| Theorem | mapenlem1 4634 | Lemma for mapen 4636. |
| Theorem | mapenlem2 4635 | Lemma for mapen 4636. |
| Theorem | mapen 4636 | Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of [Enderton] p. 139. |
| Theorem | mapdom1 4637 | Order-preserving property of set exponentiation. Theorem 6L(c) of [Enderton] p. 149. |
| Theorem | mapdom2lem 4638 | Lemma for mapdom2 4639. |
| Theorem | mapdom2 4639 | Order-preserving property of set exponentiation. Theorem 6L(d) of [Enderton] p. 149. |
| Theorem | mapxpen 4640 | Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96. |
| Theorem | xpmapenlem1 4641 | Lemma for xpmapen 4646. |
| Theorem | xpmapenlem2 4642 | Lemma for xpmapen 4646. |
| Theorem | xpmapenlem3 4643 | Lemma for xpmapen 4646. |
| Theorem | xpmapenlem4 4644 | Lemma for xpmapen 4646. |
| Theorem | xpmapenlem5 4645 | Lemma for xpmapen 4646. |
| Theorem | xpmapen 4646 | Equinumerosity law for set exponentiation of a cross product. Exercise 4.47 of [Mendelson] p. 255. |
| Theorem | mapunen 4647 | Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of [Mendelson] p. 255. |
| Theorem | pwen 4648 | If two sets are equinumerous, then their power sets are equinumerous. Proposition 10.15 of [TakeutiZaring] p. 87. |
| Theorem | ssenen 4649 | Equinumerosity of equinumerous subsets of a set. |
| Theorem | limenpsi 4650 | A limit ordinal is equinumerous to a proper subset of itself. |
| Theorem | limensuci 4651 | A limit ordinal is equinumerous to its successor. |
| Theorem | limensuc 4652 | A limit ordinal is equinumerous to its successor. |
| Pigeonhole Principle | ||
| Theorem | phplem1 4653 | Lemma for Pigeonhole Principle. If we join a natural number to itself minus an element, we end up with its successor minus the same element. |
| Theorem | phplem2 4654 | Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements. |
| Theorem | phplem3 4655 | Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. |
| Theorem | phplem4 4656 | Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. |
| Theorem | nneneq 4657 | Two equinumerous natural numbers are equal. Proposition 10.20 of [TakeutiZaring] p. 90 and its converse. Also compare Corollary 6E of [Enderton] p. 136. |
| Theorem | php 4658 | Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of [Enderton] p. 134. The theorem is so-called because you can't put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of lemmas phplem1 4653 through phplem4 4656, nneneq 4657, and this final piece of the proof. |
| Theorem | php2 4659 | Corollary of Pigeonhole Principle. |
| Theorem | php3 4660 |
Corollary of Pigeonhole Principle. If |
| Theorem | php4 4661 | Corollary of the Pigeonhole Principle php 4658: a natural number is strictly dominated by its successor. |
| Theorem | php5 4662 | Corollary of the Pigeonhole Principle php 4658: a natural number is not equinumerous to its successor. Corollary 10.21(1) of [TakeutiZaring] p. 90. |
| Finite sets | ||
| Theorem | onomeneq 4663 | An ordinal number equinumerous to a natural number is equal to it. Proposition 10.22 of [TakeutiZaring] p. 90 and its converse. |
| Theorem | onfin 4664 | An ordinal number is finite iff it is a natural number. Proposition 10.32 of [TakeutiZaring] p. 92. |
| Theorem | nndomo 4665 | Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. |
| Theorem | nnsdomo 4666 | Cardinal ordering agrees with natural number ordering. |
| Theorem | omsucdom 4667 | Strict dominance of natural numbers is the same as dominance over the successor of the smaller. |
| Theorem | sucdomi 4668 | Dominance of a set over a successor of a natural number implies strict dominance over the number. For the converse, see sucdom 4990. |
| Theorem | 0sdom1dom 4669 | Strict dominance over zero is the same as dominance over one. |
| Theorem | 1sdom2 4670 | Ordinal 1 is strictly dominated by ordinal 2. |
| Theorem | finsucdom 4671 | Strict dominance of a finite set over a natural number is the same as dominance over its successor. |
| Theorem | pssinf 4672 | A set equinumerous to a proper subset of itself is infinite. Corollary 6D(a) of [Enderton] p. 136. |
| Theorem | ominf 4673 | The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. |
| Theorem | omsdomnn 4674 |
Omega strictly dominates a natural number. Example 3 of [Enderton]
p. 146. Here we use |
| Theorem | isfinite1 4675 | Omega strictly dominates a finite set. See comment in omsdomnn 4674. |
| Theorem | infsdomnn 4676 | An infinite set strictly dominates a natural number. |
| Theorem | infn0 4677 | An infinite set is not empty. |
| Theorem | enfi 4678 | Equinmerous sets have the same finiteness. |
| Theorem | pssnn 4679 | A proper subset of a natural number is equinumerous to some smaller number. Lemma 6F of [Enderton] p. 137. |
| Theorem | ssnnfi 4680 | A subset of a natural number is finite. |
| Theorem | ssfi 4681 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. |
| Theorem | domfi 4682 | A set dominated by a finite set is finite. |
| Theorem | xpfi 4683 | The components of a non-empty finite cross product are finite. (Contributed by Paul Chapman, 11-Apr-2009.) |
| Theorem | unblem1 4684 | Lemma for unbnn 4688. After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set. |
| Theorem | unblem2 4685 |
Lemma for unbnn 4688. The value of the function |
| Theorem | unblem3 4686 |
Lemma for unbnn 4688. The value of the function |
| Theorem | unblem4 4687 |
Lemma for unbnn 4688. The function |
| Theorem | unbnn 4688 | Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. Part of the proof of Theorem 42 of [Suppes] p. 151. See unbnn3 4783 for a stronger version without the hypothesis. |
| Theorem | unbnn2 4689 | Version of unbnn 4688 that does not require a strict upper bound. |
| Theorem | isfinite2 4690 | Any set strictly dominated by the class of natural numbers is finite. Sufficiency part of Theorem 42 of [Suppes] p. 151. This theorem does not require the Axiom of Infinity. |
| Theorem | fin2inf 4691 |
This (useless) theorem, which was proved without the Axiom of Infinity,
demonstrates an artifact of our definition of strict dominance, which is
meaningful only when its arguments exist. In particular, the antecedent
cannot be satisfied unless |
| Theorem | unfilem1 4692 | Lemma for proving that the union of two finite sets is finite. |
| Theorem | unfilem2 4693 | Lemma for proving that the union of two finite sets is finite. |
| Theorem | unfilem3 4694 | Lemma for proving that the union of two finite sets is finite. |
| Theorem | unfi 4695 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. |
| Theorem | unfi2 4696 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 4695 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 4691). |
| Theorem | infcntss 4697 | Every infinite set has a denumerable subset. Similar to Exercise 8 of [TakeutiZaring] p. 91. (However, we need neither AC nor the Axiom of Infinity because of the way we express "infinite" in the antecedent.) |
| Theorem | prfi 4698 | An unordered pair is finite. |
| Theorem | unifi 4699 | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. |
| Theorem | unifi2 4700 | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 4699 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 4691). |
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |