Home | Metamath
Proof Explorer Theorem List (p. 79 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elqsecl 7801* | Membership in a quotient set by an equivalence class according to . (Contributed by Alexander van der Vekens, 12-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
Theorem | ecelqsg 7802 | Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | ecelqsi 7803 | Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | ecopqsi 7804 | "Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.) |
Theorem | qsexg 7805 | A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | qsex 7806 | A quotient set exists. (Contributed by NM, 14-Aug-1995.) |
Theorem | uniqs 7807 | The union of a quotient set. (Contributed by NM, 9-Dec-2008.) |
Theorem | qsss 7808 | A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
Theorem | uniqs2 7809 | The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.) |
Theorem | snec 7810 | The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | ecqs 7811 | Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.) |
Theorem | ecid 7812 | A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | qsid 7813 | A set is equal to its quotient set mod converse epsilon. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | ectocld 7814* | Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.) |
Theorem | ectocl 7815* | Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | elqsn0 7816 | A quotient set doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.) |
Theorem | ecelqsdm 7817 | Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.) |
Theorem | xpider 7818 | A square Cartesian product is an equivalence relation (in general it's not a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 12-Aug-2015.) |
Theorem | iiner 7819* | The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
Theorem | riiner 7820* | The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
Theorem | erinxp 7821 | A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
Theorem | ecinxp 7822 | Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.) |
Theorem | qsinxp 7823 | Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Theorem | qsdisj 7824 | Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.) |
Theorem | qsdisj2 7825* | A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.) |
Disj | ||
Theorem | qsel 7826 | If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.) |
Theorem | uniinqs 7827 | Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4457. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.) |
Theorem | qliftlem 7828* | , a function lift, is a subset of . (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | qliftrel 7829* | , a function lift, is a subset of . (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | qliftel 7830* | Elementhood in the relation . (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | qliftel1 7831* | Elementhood in the relation . (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | qliftfun 7832* | The function is the unique function defined by , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | qliftfund 7833* | The function is the unique function defined by , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | qliftfuns 7834* | The function is the unique function defined by , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | qliftf 7835* | The domain and range of the function . (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | qliftval 7836* | The value of the function . (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | ecoptocl 7837* | Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.) |
Theorem | 2ecoptocl 7838* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.) |
Theorem | 3ecoptocl 7839* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.) |
Theorem | brecop 7840* | Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.) |
Theorem | brecop2 7841 | Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis. (Contributed by NM, 13-Feb-1996.) |
Theorem | eroveu 7842* | Lemma for erov 7844 and eroprf 7845. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | erovlem 7843* | Lemma for erov 7844 and eroprf 7845. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
Theorem | erov 7844* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
Theorem | eroprf 7845* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
Theorem | erov2 7846* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | eroprf2 7847* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | ecopoveq 7848* | This is the first of several theorems about equivalence relations of the kind used in construction of fractions and signed reals, involving operations on equivalent classes of ordered pairs. This theorem expresses the relation (specified by the hypothesis) in terms of its operation . (Contributed by NM, 16-Aug-1995.) |
Theorem | ecopovsym 7849* | Assuming the operation is commutative, show that the relation , specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | ecopovtrn 7850* | Assuming that operation is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | ecopover 7851* | Assuming that operation is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is an equivalence relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof shortened by AV, 1-May-2021.) |
Theorem | ecopoverOLD 7852* | Obsolete proof of ecopover 7851 as of 1-May-2021. Assuming that operation is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is an equivalence relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | eceqoveq 7853* | Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) |
Theorem | ecovcom 7854* | Lemma used to transfer a commutative law via an equivalence relation. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
Theorem | ecovass 7855* | Lemma used to transfer an associative law via an equivalence relation. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
Theorem | ecovdi 7856* | Lemma used to transfer a distributive law via an equivalence relation. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
Syntax | cmap 7857 | Extend the definition of a class to include the mapping operation. (Read for , "the set of all functions that map from to .) |
Syntax | cpm 7858 | Extend the definition of a class to include the partial mapping operation. (Read for , "the set of all partial functions that map from to .) |
Definition | df-map 7859* | Define the mapping operation or set exponentiation. The set of all functions that map from to is written (see mapval 7869). Many authors write followed by as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring] p. 95). Other authors show as a prefixed superscript, which is read " pre " (e.g., definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(, ) for our . The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003.) |
Definition | df-pm 7860* | Define the partial mapping operation. A partial function from to is a function from a subset of to . The set of all partial functions from to is written (see pmvalg 7868). A notation for this operation apparently does not appear in the literature. We use to distinguish it from the less general set exponentiation operation (df-map 7859) . See mapsspm 7891 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.) |
Theorem | mapprc 7861* | When is a proper class, the class of all functions mapping to is empty. Exercise 4.41 of [Mendelson] p. 255. (Contributed by NM, 8-Dec-2003.) |
Theorem | pmex 7862* | The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.) |
Theorem | mapex 7863* | The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.) |
Theorem | fnmap 7864 | Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | fnpm 7865 | Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.) |
Theorem | reldmmap 7866 | Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
Theorem | mapvalg 7867* | The value of set exponentiation. is the set of all functions that map from to . Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | pmvalg 7868* | The value of the partial mapping operation. is the set of all partial functions that map from to . (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | mapval 7869* | The value of set exponentiation (inference version). is the set of all functions that map from to . Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.) |
Theorem | elmapg 7870 | Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.) |
Theorem | elmapd 7871 | Deduction form of elmapg 7870. (Contributed by BJ, 11-Apr-2020.) |
Theorem | mapdm0 7872 | The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020.) (Proof shortened by Thierry Arnoux, 3-Dec-2021.) |
Theorem | elpmg 7873 | The predicate "is a partial function." (Contributed by Mario Carneiro, 14-Nov-2013.) |
Theorem | elpm2g 7874 | The predicate "is a partial function." (Contributed by NM, 31-Dec-2013.) |
Theorem | elpm2r 7875 | Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013.) |
Theorem | elpmi 7876 | A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
Theorem | pmfun 7877 | A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | elmapex 7878 | Eliminate antecedent for mapping theorems: domain can be taken to be a set. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
Theorem | elmapi 7879 | A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Theorem | elmapfn 7880 | A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.) |
Theorem | elmapfun 7881 | A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
Theorem | elmapssres 7882 | A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.) |
Theorem | fpmg 7883 | A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
Theorem | pmss12g 7884 | Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
Theorem | pmresg 7885 | Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
Theorem | elmap 7886 | Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.) |
Theorem | mapval2 7887* | Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.) |
Theorem | elpm 7888 | The predicate "is a partial function." (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
Theorem | elpm2 7889 | The predicate "is a partial function." (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
Theorem | fpm 7890 | A total function is a partial function. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
Theorem | mapsspm 7891 | Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.) |
Theorem | pmsspw 7892 | Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Theorem | mapsspw 7893 | Set exponentiation is a subset of the power set of the Cartesian product of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | fvmptmap 7894* | Special case of fvmpt 6282 for operator theorems. (Contributed by NM, 27-Nov-2007.) |
Theorem | map0e 7895 | Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | map0b 7896 | Set exponentiation with an empty base is the empty set, provided the exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | map0g 7897 | Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by Mario Carneiro, 30-Apr-2015.) |
Theorem | map0 7898 | Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) |
Theorem | mapsn 7899* | The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) |
Theorem | mapss 7900 | Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |