Home | Intuitionistic Logic Explorer Theorem List (p. 69 of 137) | < 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 | snnen2og 6801 | A singleton is never equinumerous with the ordinal number 2. If is a proper class, see snnen2oprc 6802. (Contributed by Jim Kingdon, 1-Sep-2021.) |
Theorem | snnen2oprc 6802 | A singleton is never equinumerous with the ordinal number 2. If is a set, see snnen2og 6801. (Contributed by Jim Kingdon, 1-Sep-2021.) |
Theorem | 1nen2 6803 | One and two are not equinumerous. (Contributed by Jim Kingdon, 25-Jan-2022.) |
Theorem | phplem4dom 6804 | Dominance of successors implies dominance of the original natural numbers. (Contributed by Jim Kingdon, 1-Sep-2021.) |
Theorem | php5dom 6805 | A natural number does not dominate its successor. (Contributed by Jim Kingdon, 1-Sep-2021.) |
Theorem | nndomo 6806 | Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.) |
Theorem | phpm 6807* | 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 6794 through phplem4 6797, nneneq 6799, and this final piece of the proof. (Contributed by NM, 29-May-1998.) |
Theorem | phpelm 6808 | Pigeonhole Principle. A natural number is not equinumerous to an element of itself. (Contributed by Jim Kingdon, 6-Sep-2021.) |
Theorem | phplem4on 6809 | Equinumerosity of successors of an ordinal and a natural number implies equinumerosity of the originals. (Contributed by Jim Kingdon, 5-Sep-2021.) |
Theorem | fict 6810 | A finite set is dominated by . Also see finct 7054. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
Theorem | fidceq 6811 | 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 6812 | All decrements of a finite set are equinumerous. (Contributed by Jim Kingdon, 9-Sep-2021.) |
Theorem | fidifsnid 6813 | 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 3702 from subset to equality when the set is finite. (Contributed by Jim Kingdon, 9-Sep-2021.) |
Theorem | nnfi 6814 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
Theorem | enfi 6815 | Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.) |
Theorem | enfii 6816 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) |
Theorem | ssfilem 6817* | Lemma for ssfiexmid 6818. (Contributed by Jim Kingdon, 3-Feb-2022.) |
Theorem | ssfiexmid 6818* | 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 6819* | 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 6820* | If any set dominated by a finite set is finite, excluded middle follows. (Contributed by Jim Kingdon, 3-Feb-2022.) |
Theorem | dif1en 6821 | 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 6822 | Subtracting one element from each of two equinumerous finite sets. (Contributed by Jim Kingdon, 5-Jun-2022.) |
Theorem | fiunsnnn 6823 | Adding one element to a finite set which is equinumerous to a natural number. (Contributed by Jim Kingdon, 13-Sep-2021.) |
Theorem | php5fin 6824 | A finite set is not equinumerous to a set which adds one element. (Contributed by Jim Kingdon, 13-Sep-2021.) |
Theorem | fisbth 6825 | Schroeder-Bernstein Theorem for finite sets. (Contributed by Jim Kingdon, 12-Sep-2021.) |
Theorem | 0fin 6826 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
Theorem | fin0 6827* | A nonempty finite set has at least one element. (Contributed by Jim Kingdon, 10-Sep-2021.) |
Theorem | fin0or 6828* | A finite set is either empty or inhabited. (Contributed by Jim Kingdon, 30-Sep-2021.) |
Theorem | diffitest 6829* | 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 6830* | 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 6831* | 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 6832* | Variation of findcard2 6831 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 6833* | Deduction version of findcard2 6831. If you also need (which doesn't come for free due to ssfiexmid 6818), use findcard2sd 6834 instead. (Contributed by SO, 16-Jul-2018.) |
Theorem | findcard2sd 6834* | Deduction form of finite set induction . (Contributed by Jim Kingdon, 14-Sep-2021.) |
Theorem | diffisn 6835 | Subtracting a singleton from a finite set produces a finite set. (Contributed by Jim Kingdon, 11-Sep-2021.) |
Theorem | diffifi 6836 | Subtracting one finite set from another produces a finite set. (Contributed by Jim Kingdon, 8-Sep-2021.) |
Theorem | infnfi 6837 | An infinite set is not finite. (Contributed by Jim Kingdon, 20-Feb-2022.) |
Theorem | ominf 6838 | 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 6709. (Contributed by NM, 2-Jun-1998.) |
Theorem | isinfinf 6839* | An infinite set contains subsets of arbitrarily large finite cardinality. (Contributed by Jim Kingdon, 15-Jun-2022.) |
Theorem | ac6sfi 6840* | 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 6841* | A trichotomous order is decidable. (Contributed by Jim Kingdon, 5-Sep-2022.) |
DECID | ||
Theorem | fimax2gtrilemstep 6842* | Lemma for fimax2gtri 6843. The induction step. (Contributed by Jim Kingdon, 5-Sep-2022.) |
Theorem | fimax2gtri 6843* | A finite set has a maximum under a trichotomous order. (Contributed by Jim Kingdon, 5-Sep-2022.) |
Theorem | finexdc 6844* | Decidability of existence, over a finite set and defined by a decidable proposition. (Contributed by Jim Kingdon, 12-Jul-2022.) |
DECID DECID | ||
Theorem | dfrex2fin 6845* | 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 6846* | An infinite set is inhabited. (Contributed by Jim Kingdon, 18-Feb-2022.) |
Theorem | infn0 6847 | An infinite set is not empty. (Contributed by NM, 23-Oct-2004.) |
Theorem | inffiexmid 6848* | If any given set is either finite or infinite, excluded middle follows. (Contributed by Jim Kingdon, 15-Jun-2022.) |
Theorem | en2eqpr 6849 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
Theorem | exmidpw 6850 | 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 | exmidpweq 6851 | Excluded middle is equivalent to the power set of being . (Contributed by Jim Kingdon, 28-Jul-2024.) |
EXMID | ||
Theorem | pw1fin 6852 | Excluded middle is equivalent to the power set of being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.) |
EXMID | ||
Theorem | pw1dc0el 6853 | Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.) |
EXMID DECID | ||
Theorem | ss1o0el1o 6854 | Reformulation of ss1o0el1 4158 using instead of . (Contributed by BJ, 9-Aug-2024.) |
Theorem | pw1dc1 6855 | If, in the set of truth values (the powerset of 1o), equality to 1o is decidable, then excluded middle holds (and conversely). (Contributed by BJ and Jim Kingdon, 8-Aug-2024.) |
EXMID DECID | ||
Theorem | fientri3 6856 | Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.) |
Theorem | nnwetri 6857* | 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 6858 | Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.) |
Theorem | unfiexmid 6859* | 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 6860 | Adding a singleton to a finite set yields a finite set. (Contributed by Jim Kingdon, 3-Feb-2022.) |
Theorem | unsnfidcex 6861 | The condition in unsnfi 6860. This is intended to show that unsnfi 6860 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 6862 | The condition in unsnfi 6860. This is intended to show that unsnfi 6860 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 6863 | The union of two disjoint finite sets is finite. (Contributed by Jim Kingdon, 25-Feb-2022.) |
Theorem | undifdcss 6864* | Union of complementary parts into whole and decidability. (Contributed by Jim Kingdon, 17-Jun-2022.) |
DECID | ||
Theorem | undifdc 6865* | Union of complementary parts into whole. This is a case where we can strengthen undifss 3474 from subset to equality. (Contributed by Jim Kingdon, 17-Jun-2022.) |
DECID | ||
Theorem | undiffi 6866 | Union of complementary parts into whole. This is a case where we can strengthen undifss 3474 from subset to equality. (Contributed by Jim Kingdon, 2-Mar-2022.) |
Theorem | unfiin 6867 | The union of two finite sets is finite if their intersection is. (Contributed by Jim Kingdon, 2-Mar-2022.) |
Theorem | prfidisj 6868 | A pair is finite if it consists of two unequal sets. For the case where , see snfig 6756. For the cases where one or both is a proper class, see prprc1 3667, prprc2 3668, or prprc 3669. (Contributed by Jim Kingdon, 31-May-2022.) |
Theorem | tpfidisj 6869 | A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.) |
Theorem | fiintim 6870* |
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 6871 | 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 6872 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
Theorem | fisseneq 6873 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
Theorem | phpeqd 6874 | Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6807 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
Theorem | ssfirab 6875* | 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 6876* | 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 6877 | An ordinal which is a singleton is . (Contributed by Jim Kingdon, 19-Oct-2021.) |
Theorem | fnfi 6878 | A version of fnex 5688 for finite sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) |
Theorem | fundmfi 6879 | The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | fundmfibi 6880 | A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.) |
Theorem | resfnfinfinss 6881 | 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 6882 | If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | funrnfi 6883 | The range of a finite relation is finite if its converse is a function. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | f1ofi 6884 | If a 1-1 and onto function has a finite domain, its range is finite. (Contributed by Jim Kingdon, 21-Feb-2022.) |
Theorem | f1dmvrnfibi 6885 | A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 6886. (Contributed by AV, 10-Jan-2020.) |
Theorem | f1vrnfibi 6886 | A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 6885. (Contributed by AV, 10-Jan-2020.) |
Theorem | iunfidisj 6887* | 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 6888 | Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) |
Theorem | en1eqsn 6889 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) |
Theorem | en1eqsnbi 6890 | 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 6891* | A case where the antecedent of snexg 4145 is not needed. The class is from dcextest 4539. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.) |
Theorem | preimaf1ofi 6892 | The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.) |
Theorem | fidcenumlemim 6893* | Lemma for fidcenum 6897. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
Theorem | fidcenumlemrks 6894* | Lemma for fidcenum 6897. Induction step for fidcenumlemrk 6895. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
Theorem | fidcenumlemrk 6895* | Lemma for fidcenum 6897. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
Theorem | fidcenumlemr 6896* | Lemma for fidcenum 6897. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
Theorem | fidcenum 6897* | 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 6898* | Lemma for isbth 6908. (Contributed by NM, 22-Mar-1998.) |
Theorem | sbthlem2 6899* | Lemma for isbth 6908. (Contributed by NM, 22-Mar-1998.) |
Theorem | sbthlemi3 6900* | Lemma for isbth 6908. (Contributed by NM, 22-Mar-1998.) |
EXMID |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |