Home | Intuitionistic Logic Explorer Theorem List (p. 68 of 130) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phplem3g 6701 | A natural number is equinumerous to its successor minus any element of the successor. Version of phplem3 6699 with unnecessary hypotheses removed. (Contributed by Jim Kingdon, 1-Sep-2021.) |
Theorem | nneneq 6702 | Two equinumerous natural numbers are equal. Proposition 10.20 of [TakeutiZaring] p. 90 and its converse. Also compare Corollary 6E of [Enderton] p. 136. (Contributed by NM, 28-May-1998.) |
Theorem | php5 6703 | A natural number is not equinumerous to its successor. Corollary 10.21(1) of [TakeutiZaring] p. 90. (Contributed by NM, 26-Jul-2004.) |
Theorem | snnen2og 6704 | A singleton is never equinumerous with the ordinal number 2. If is a proper class, see snnen2oprc 6705. (Contributed by Jim Kingdon, 1-Sep-2021.) |
Theorem | snnen2oprc 6705 | A singleton is never equinumerous with the ordinal number 2. If is a set, see snnen2og 6704. (Contributed by Jim Kingdon, 1-Sep-2021.) |
Theorem | 1nen2 6706 | One and two are not equinumerous. (Contributed by Jim Kingdon, 25-Jan-2022.) |
Theorem | phplem4dom 6707 | Dominance of successors implies dominance of the original natural numbers. (Contributed by Jim Kingdon, 1-Sep-2021.) |
Theorem | php5dom 6708 | A natural number does not dominate its successor. (Contributed by Jim Kingdon, 1-Sep-2021.) |
Theorem | nndomo 6709 | Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.) |
Theorem | phpm 6710* | Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. By "proper subset" here we mean that there is an element which is in the natural number and not in the subset, or in symbols (which is stronger than not being equal in the absence of excluded middle). 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 6697 through phplem4 6700, nneneq 6702, and this final piece of the proof. (Contributed by NM, 29-May-1998.) |
Theorem | phpelm 6711 | Pigeonhole Principle. A natural number is not equinumerous to an element of itself. (Contributed by Jim Kingdon, 6-Sep-2021.) |
Theorem | phplem4on 6712 | Equinumerosity of successors of an ordinal and a natural number implies equinumerosity of the originals. (Contributed by Jim Kingdon, 5-Sep-2021.) |
Theorem | fict 6713 | A finite set is dominated by . Also see finct 6951. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
Theorem | fidceq 6714 | Equality of members of a finite set is decidable. This may be counterintuitive: cannot any two sets be elements of a finite set? Well, to show, for example, that is finite would require showing it is equinumerous to or to but to show that you'd need to know or , respectively. (Contributed by Jim Kingdon, 5-Sep-2021.) |
DECID | ||
Theorem | fidifsnen 6715 | All decrements of a finite set are equinumerous. (Contributed by Jim Kingdon, 9-Sep-2021.) |
Theorem | fidifsnid 6716 | If we remove a single element from a finite set then put it back in, we end up with the original finite set. This strengthens difsnss 3630 from subset to equality when the set is finite. (Contributed by Jim Kingdon, 9-Sep-2021.) |
Theorem | nnfi 6717 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
Theorem | enfi 6718 | Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.) |
Theorem | enfii 6719 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) |
Theorem | ssfilem 6720* | Lemma for ssfiexmid 6721. (Contributed by Jim Kingdon, 3-Feb-2022.) |
Theorem | ssfiexmid 6721* | If any subset of a finite set is finite, excluded middle follows. One direction of Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 19-May-2020.) |
Theorem | infiexmid 6722* | If the intersection of any finite set and any other set is finite, excluded middle follows. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | domfiexmid 6723* | If any set dominated by a finite set is finite, excluded middle follows. (Contributed by Jim Kingdon, 3-Feb-2022.) |
Theorem | dif1en 6724 | If a set is equinumerous to the successor of a natural number , then with an element removed is equinumerous to . (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) |
Theorem | dif1enen 6725 | Subtracting one element from each of two equinumerous finite sets. (Contributed by Jim Kingdon, 5-Jun-2022.) |
Theorem | fiunsnnn 6726 | Adding one element to a finite set which is equinumerous to a natural number. (Contributed by Jim Kingdon, 13-Sep-2021.) |
Theorem | php5fin 6727 | A finite set is not equinumerous to a set which adds one element. (Contributed by Jim Kingdon, 13-Sep-2021.) |
Theorem | fisbth 6728 | Schroeder-Bernstein Theorem for finite sets. (Contributed by Jim Kingdon, 12-Sep-2021.) |
Theorem | 0fin 6729 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
Theorem | fin0 6730* | A nonempty finite set has at least one element. (Contributed by Jim Kingdon, 10-Sep-2021.) |
Theorem | fin0or 6731* | A finite set is either empty or inhabited. (Contributed by Jim Kingdon, 30-Sep-2021.) |
Theorem | diffitest 6732* | If subtracting any set from a finite set gives a finite set, any proposition of the form is decidable. This is not a proof of full excluded middle, but it is close enough to show we won't be able to prove . (Contributed by Jim Kingdon, 8-Sep-2021.) |
Theorem | findcard 6733* | Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | findcard2 6734* | Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.) |
Theorem | findcard2s 6735* | Variation of findcard2 6734 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.) |
Theorem | findcard2d 6736* | Deduction version of findcard2 6734. If you also need (which doesn't come for free due to ssfiexmid 6721), use findcard2sd 6737 instead. (Contributed by SO, 16-Jul-2018.) |
Theorem | findcard2sd 6737* | Deduction form of finite set induction . (Contributed by Jim Kingdon, 14-Sep-2021.) |
Theorem | diffisn 6738 | Subtracting a singleton from a finite set produces a finite set. (Contributed by Jim Kingdon, 11-Sep-2021.) |
Theorem | diffifi 6739 | Subtracting one finite set from another produces a finite set. (Contributed by Jim Kingdon, 8-Sep-2021.) |
Theorem | infnfi 6740 | An infinite set is not finite. (Contributed by Jim Kingdon, 20-Feb-2022.) |
Theorem | ominf 6741 | The set of natural numbers is not finite. Although we supply this theorem because we can, the more natural way to express " is infinite" is which is an instance of domrefg 6613. (Contributed by NM, 2-Jun-1998.) |
Theorem | isinfinf 6742* | An infinite set contains subsets of arbitrarily large finite cardinality. (Contributed by Jim Kingdon, 15-Jun-2022.) |
Theorem | ac6sfi 6743* | Existence of a choice function for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
Theorem | tridc 6744* | A trichotomous order is decidable. (Contributed by Jim Kingdon, 5-Sep-2022.) |
DECID | ||
Theorem | fimax2gtrilemstep 6745* | Lemma for fimax2gtri 6746. The induction step. (Contributed by Jim Kingdon, 5-Sep-2022.) |
Theorem | fimax2gtri 6746* | A finite set has a maximum under a trichotomous order. (Contributed by Jim Kingdon, 5-Sep-2022.) |
Theorem | finexdc 6747* | Decidability of existence, over a finite set and defined by a decidable proposition. (Contributed by Jim Kingdon, 12-Jul-2022.) |
DECID DECID | ||
Theorem | dfrex2fin 6748* | Relationship between universal and existential quantifiers over a finite set. Remark in Section 2.2.1 of [Pierik], p. 8. Although Pierik does not mention the decidability condition explicitly, it does say "only finitely many x to check" which means there must be some way of checking each value of x. (Contributed by Jim Kingdon, 11-Jul-2022.) |
DECID | ||
Theorem | infm 6749* | An infinite set is inhabited. (Contributed by Jim Kingdon, 18-Feb-2022.) |
Theorem | infn0 6750 | An infinite set is not empty. (Contributed by NM, 23-Oct-2004.) |
Theorem | inffiexmid 6751* | If any given set is either finite or infinite, excluded middle follows. (Contributed by Jim Kingdon, 15-Jun-2022.) |
Theorem | en2eqpr 6752 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
Theorem | exmidpw 6753 | Excluded middle is equivalent to the power set of having two elements. Remark of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 30-Jun-2022.) |
EXMID | ||
Theorem | fientri3 6754 | Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.) |
Theorem | nnwetri 6755* | A natural number is well-ordered by . More specifically, this order both satisfies and is trichotomous. (Contributed by Jim Kingdon, 25-Sep-2021.) |
Theorem | onunsnss 6756 | Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.) |
Theorem | unfiexmid 6757* | If the union of any two finite sets is finite, excluded middle follows. Remark 8.1.17 of [AczelRathjen], p. 74. (Contributed by Mario Carneiro and Jim Kingdon, 5-Mar-2022.) |
Theorem | unsnfi 6758 | Adding a singleton to a finite set yields a finite set. (Contributed by Jim Kingdon, 3-Feb-2022.) |
Theorem | unsnfidcex 6759 | The condition in unsnfi 6758. This is intended to show that unsnfi 6758 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.) |
DECID | ||
Theorem | unsnfidcel 6760 | The condition in unsnfi 6758. This is intended to show that unsnfi 6758 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.) |
DECID | ||
Theorem | unfidisj 6761 | The union of two disjoint finite sets is finite. (Contributed by Jim Kingdon, 25-Feb-2022.) |
Theorem | undifdcss 6762* | Union of complementary parts into whole and decidability. (Contributed by Jim Kingdon, 17-Jun-2022.) |
DECID | ||
Theorem | undifdc 6763* | Union of complementary parts into whole. This is a case where we can strengthen undifss 3407 from subset to equality. (Contributed by Jim Kingdon, 17-Jun-2022.) |
DECID | ||
Theorem | undiffi 6764 | Union of complementary parts into whole. This is a case where we can strengthen undifss 3407 from subset to equality. (Contributed by Jim Kingdon, 2-Mar-2022.) |
Theorem | unfiin 6765 | The union of two finite sets is finite if their intersection is. (Contributed by Jim Kingdon, 2-Mar-2022.) |
Theorem | prfidisj 6766 | A pair is finite if it consists of two unequal sets. For the case where , see snfig 6660. For the cases where one or both is a proper class, see prprc1 3595, prprc2 3596, or prprc 3597. (Contributed by Jim Kingdon, 31-May-2022.) |
Theorem | tpfidisj 6767 | A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.) |
Theorem | fiintim 6768* |
If a class is closed under pairwise intersections, then it is closed
under nonempty finite intersections. The converse would appear to
require an additional condition, such as and not being
equal, or
having decidable equality.
This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.) |
Theorem | xpfi 6769 | The Cartesian product of two finite sets is finite. Lemma 8.1.16 of [AczelRathjen], p. 74. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) |
Theorem | 3xpfi 6770 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
Theorem | fisseneq 6771 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
Theorem | ssfirab 6772* | A subset of a finite set is finite if it is defined by a decidable property. (Contributed by Jim Kingdon, 27-May-2022.) |
DECID | ||
Theorem | ssfidc 6773* | A subset of a finite set is finite if membership in the subset is decidable. (Contributed by Jim Kingdon, 27-May-2022.) |
DECID | ||
Theorem | snon0 6774 | An ordinal which is a singleton is . (Contributed by Jim Kingdon, 19-Oct-2021.) |
Theorem | fnfi 6775 | A version of fnex 5594 for finite sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) |
Theorem | fundmfi 6776 | The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | fundmfibi 6777 | A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.) |
Theorem | resfnfinfinss 6778 | The restriction of a function to a finite subset of its domain is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.) |
Theorem | relcnvfi 6779 | If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | funrnfi 6780 | The range of a finite relation is finite if its converse is a function. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | f1ofi 6781 | If a 1-1 and onto function has a finite domain, its range is finite. (Contributed by Jim Kingdon, 21-Feb-2022.) |
Theorem | f1dmvrnfibi 6782 | A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 6783. (Contributed by AV, 10-Jan-2020.) |
Theorem | f1vrnfibi 6783 | A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 6782. (Contributed by AV, 10-Jan-2020.) |
Theorem | iunfidisj 6784* | The finite union of disjoint finite sets is finite. Note that depends on , i.e. can be thought of as . (Contributed by NM, 23-Mar-2006.) (Revised by Jim Kingdon, 7-Oct-2022.) |
Disj | ||
Theorem | f1finf1o 6785 | Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) |
Theorem | en1eqsn 6786 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) |
Theorem | en1eqsnbi 6787 | A set containing an element has exactly one element iff it is a singleton. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
Theorem | snexxph 6788* | A case where the antecedent of snexg 4066 is not needed. The class is from dcextest 4453. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.) |
Theorem | preimaf1ofi 6789 | The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.) |
Theorem | fidcenumlemim 6790* | Lemma for fidcenum 6794. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
Theorem | fidcenumlemrks 6791* | Lemma for fidcenum 6794. Induction step for fidcenumlemrk 6792. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
Theorem | fidcenumlemrk 6792* | Lemma for fidcenum 6794. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
Theorem | fidcenumlemr 6793* | Lemma for fidcenum 6794. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
Theorem | fidcenum 6794* | A set is finite if and only if it has decidable equality and is finitely enumerable. Proposition 8.1.11 of [AczelRathjen], p. 72. The definition of "finitely enumerable" as is Definition 8.1.4 of [AczelRathjen], p. 71. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
Theorem | sbthlem1 6795* | Lemma for isbth 6805. (Contributed by NM, 22-Mar-1998.) |
Theorem | sbthlem2 6796* | Lemma for isbth 6805. (Contributed by NM, 22-Mar-1998.) |
Theorem | sbthlemi3 6797* | Lemma for isbth 6805. (Contributed by NM, 22-Mar-1998.) |
EXMID | ||
Theorem | sbthlemi4 6798* | Lemma for isbth 6805. (Contributed by NM, 27-Mar-1998.) |
EXMID | ||
Theorem | sbthlemi5 6799* | Lemma for isbth 6805. (Contributed by NM, 22-Mar-1998.) |
EXMID | ||
Theorem | sbthlemi6 6800* | Lemma for isbth 6805. (Contributed by NM, 27-Mar-1998.) |
EXMID |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |