Home | Intuitionistic Logic Explorer Theorem List (p. 69 of 133) | < 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 | unsnfidcex 6801 | The condition in unsnfi 6800. This is intended to show that unsnfi 6800 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 6802 | The condition in unsnfi 6800. This is intended to show that unsnfi 6800 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 6803 | The union of two disjoint finite sets is finite. (Contributed by Jim Kingdon, 25-Feb-2022.) |
Theorem | undifdcss 6804* | Union of complementary parts into whole and decidability. (Contributed by Jim Kingdon, 17-Jun-2022.) |
DECID | ||
Theorem | undifdc 6805* | Union of complementary parts into whole. This is a case where we can strengthen undifss 3438 from subset to equality. (Contributed by Jim Kingdon, 17-Jun-2022.) |
DECID | ||
Theorem | undiffi 6806 | Union of complementary parts into whole. This is a case where we can strengthen undifss 3438 from subset to equality. (Contributed by Jim Kingdon, 2-Mar-2022.) |
Theorem | unfiin 6807 | The union of two finite sets is finite if their intersection is. (Contributed by Jim Kingdon, 2-Mar-2022.) |
Theorem | prfidisj 6808 | A pair is finite if it consists of two unequal sets. For the case where , see snfig 6701. For the cases where one or both is a proper class, see prprc1 3626, prprc2 3627, or prprc 3628. (Contributed by Jim Kingdon, 31-May-2022.) |
Theorem | tpfidisj 6809 | A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.) |
Theorem | fiintim 6810* |
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 6811 | 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 6812 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
Theorem | fisseneq 6813 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
Theorem | phpeqd 6814 | Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6752 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
Theorem | ssfirab 6815* | 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 6816* | 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 6817 | An ordinal which is a singleton is . (Contributed by Jim Kingdon, 19-Oct-2021.) |
Theorem | fnfi 6818 | A version of fnex 5635 for finite sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) |
Theorem | fundmfi 6819 | The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | fundmfibi 6820 | A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.) |
Theorem | resfnfinfinss 6821 | 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 6822 | If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | funrnfi 6823 | The range of a finite relation is finite if its converse is a function. (Contributed by Jim Kingdon, 5-Feb-2022.) |
Theorem | f1ofi 6824 | If a 1-1 and onto function has a finite domain, its range is finite. (Contributed by Jim Kingdon, 21-Feb-2022.) |
Theorem | f1dmvrnfibi 6825 | A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 6826. (Contributed by AV, 10-Jan-2020.) |
Theorem | f1vrnfibi 6826 | A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 6825. (Contributed by AV, 10-Jan-2020.) |
Theorem | iunfidisj 6827* | 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 6828 | Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) |
Theorem | en1eqsn 6829 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) |
Theorem | en1eqsnbi 6830 | 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 6831* | A case where the antecedent of snexg 4103 is not needed. The class is from dcextest 4490. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.) |
Theorem | preimaf1ofi 6832 | The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.) |
Theorem | fidcenumlemim 6833* | Lemma for fidcenum 6837. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
Theorem | fidcenumlemrks 6834* | Lemma for fidcenum 6837. Induction step for fidcenumlemrk 6835. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
Theorem | fidcenumlemrk 6835* | Lemma for fidcenum 6837. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
Theorem | fidcenumlemr 6836* | Lemma for fidcenum 6837. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
Theorem | fidcenum 6837* | 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 6838* | Lemma for isbth 6848. (Contributed by NM, 22-Mar-1998.) |
Theorem | sbthlem2 6839* | Lemma for isbth 6848. (Contributed by NM, 22-Mar-1998.) |
Theorem | sbthlemi3 6840* | Lemma for isbth 6848. (Contributed by NM, 22-Mar-1998.) |
EXMID | ||
Theorem | sbthlemi4 6841* | Lemma for isbth 6848. (Contributed by NM, 27-Mar-1998.) |
EXMID | ||
Theorem | sbthlemi5 6842* | Lemma for isbth 6848. (Contributed by NM, 22-Mar-1998.) |
EXMID | ||
Theorem | sbthlemi6 6843* | Lemma for isbth 6848. (Contributed by NM, 27-Mar-1998.) |
EXMID | ||
Theorem | sbthlem7 6844* | Lemma for isbth 6848. (Contributed by NM, 27-Mar-1998.) |
Theorem | sbthlemi8 6845* | Lemma for isbth 6848. (Contributed by NM, 27-Mar-1998.) |
EXMID | ||
Theorem | sbthlemi9 6846* | Lemma for isbth 6848. (Contributed by NM, 28-Mar-1998.) |
EXMID | ||
Theorem | sbthlemi10 6847* | Lemma for isbth 6848. (Contributed by NM, 28-Mar-1998.) |
EXMID | ||
Theorem | isbth 6848 | Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This theorem states that if set is smaller (has lower cardinality) than and vice-versa, then and are equinumerous (have the same cardinality). The interesting thing is that this can be proved without invoking the Axiom of Choice, as we do here, but the proof as you can see is quite difficult. (The theorem can be proved more easily if we allow AC.) The main proof consists of lemmas sbthlem1 6838 through sbthlemi10 6847; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 6847. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level. Note that Suppes' proof, which is credited to J. M. Whitaker, does not require the Axiom of Infinity. The proof does require the law of the excluded middle which cannot be avoided as shown at exmidsbthr 13207. (Contributed by NM, 8-Jun-1998.) |
EXMID | ||
Syntax | cfi 6849 | Extend class notation with the function whose value is the class of finite intersections of the elements of a given set. |
Definition | df-fi 6850* | Function whose value is the class of finite intersections of the elements of the argument. Note that the empty intersection being the universal class, hence a proper class, it cannot be an element of that class. Therefore, the function value is the class of nonempty finite intersections of elements of the argument (see elfi2 6853). (Contributed by FL, 27-Apr-2008.) |
Theorem | fival 6851* | The set of all the finite intersections of the elements of . (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
Theorem | elfi 6852* | Specific properties of an element of . (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
Theorem | elfi2 6853* | The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.) |
Theorem | elfir 6854 | Sufficient condition for an element of . (Contributed by Mario Carneiro, 24-Nov-2013.) |
Theorem | ssfii 6855 | Any element of a set is the intersection of a finite subset of . (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
Theorem | fi0 6856 | The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.) |
Theorem | fieq0 6857 | A set is empty iff the class of all the finite intersections of that set is empty. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
Theorem | fiss 6858 | Subset relationship for function . (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
Theorem | fiuni 6859 | The union of the finite intersections of a set is simply the union of the set itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
Theorem | fipwssg 6860 | If a set is a family of subsets of some base set, then so is its finite intersection. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
Theorem | fifo 6861* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
Syntax | csup 6862 | Extend class notation to include supremum of class . Here is ordinarily a relation that strictly orders class . For example, could be 'less than' and could be the set of real numbers. |
Syntax | cinf 6863 | Extend class notation to include infimum of class . Here is ordinarily a relation that strictly orders class . For example, could be 'less than' and could be the set of real numbers. |
inf | ||
Definition | df-sup 6864* | Define the supremum of class . It is meaningful when is a relation that strictly orders and when the supremum exists. (Contributed by NM, 22-May-1999.) |
Definition | df-inf 6865 | Define the infimum of class . It is meaningful when is a relation that strictly orders and when the infimum exists. For example, could be 'less than', could be the set of real numbers, and could be the set of all positive reals; in this case the infimum is 0. The infimum is defined as the supremum using the converse ordering relation. In the given example, 0 is the supremum of all reals (greatest real number) for which all positive reals are greater. (Contributed by AV, 2-Sep-2020.) |
inf | ||
Theorem | supeq1 6866 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
Theorem | supeq1d 6867 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | supeq1i 6868 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | supeq2 6869 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | supeq3 6870 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
Theorem | supeq123d 6871 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
Theorem | nfsup 6872 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
Theorem | supmoti 6873* | Any class has at most one supremum in (where is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 7837) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.) |
Theorem | supeuti 6874* | A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by Jim Kingdon, 23-Nov-2021.) |
Theorem | supval2ti 6875* | Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
Theorem | eqsupti 6876* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
Theorem | eqsuptid 6877* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | supclti 6878* | A supremum belongs to its base class (closure law). See also supubti 6879 and suplubti 6880. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | supubti 6879* |
A supremum is an upper bound. See also supclti 6878 and suplubti 6880.
This proof demonstrates how to expand an iota-based definition (df-iota 5083) using riotacl2 5736. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | suplubti 6880* | A supremum is the least upper bound. See also supclti 6878 and supubti 6879. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | suplub2ti 6881* | Bidirectional form of suplubti 6880. (Contributed by Jim Kingdon, 17-Jan-2022.) |
Theorem | supelti 6882* | Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
Theorem | sup00 6883 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
Theorem | supmaxti 6884* | The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | supsnti 6885* | The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.) |
Theorem | isotilem 6886* | Lemma for isoti 6887. (Contributed by Jim Kingdon, 26-Nov-2021.) |
Theorem | isoti 6887* | An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.) |
Theorem | supisolem 6888* | Lemma for supisoti 6890. (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | supisoex 6889* | Lemma for supisoti 6890. (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | supisoti 6890* | Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.) |
Theorem | infeq1 6891 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq1d 6892 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq1i 6893 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq2 6894 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq3 6895 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq123d 6896 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | nfinf 6897 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
inf | ||
Theorem | cnvinfex 6898* | Two ways of expressing existence of an infimum (one in terms of converse). (Contributed by Jim Kingdon, 17-Dec-2021.) |
Theorem | cnvti 6899* | If a relation satisfies a condition corresponding to tightness of an apartness generated by an order, so does its converse. (Contributed by Jim Kingdon, 17-Dec-2021.) |
Theorem | eqinfti 6900* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
inf |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |