Home | Metamath
Proof Explorer Theorem List (p. 73 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 | elxp7 7201 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7110. (Contributed by NM, 19-Aug-2006.) |
Theorem | eqopi 7202 | Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.) |
Theorem | xp2 7203* | Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.) |
Theorem | unielxp 7204 | The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006.) |
Theorem | 1st2nd2 7205 | Reconstruction of a member of a Cartesian product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013.) |
Theorem | 1st2ndb 7206 | Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014.) |
Theorem | xpopth 7207 | An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007.) |
Theorem | eqop 7208 | Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
Theorem | eqop2 7209 | Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.) |
Theorem | op1steq 7210* | Two ways of expressing that an element is the first member of an ordered pair. (Contributed by NM, 22-Sep-2013.) (Revised by Mario Carneiro, 23-Feb-2014.) |
Theorem | el2xptp 7211* | A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
Theorem | el2xptp0 7212 | A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
Theorem | 2nd1st 7213 | Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.) |
Theorem | 1st2nd 7214 | Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006.) |
Theorem | 1stdm 7215 | The first ordered pair component of a member of a relation belongs to the domain of the relation. (Contributed by NM, 17-Sep-2006.) |
Theorem | 2ndrn 7216 | The second ordered pair component of a member of a relation belongs to the range of the relation. (Contributed by NM, 17-Sep-2006.) |
Theorem | 1st2ndbr 7217 | Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.) |
Theorem | releldm2 7218* | Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
Theorem | reldm 7219* | An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
Theorem | sbcopeq1a 7220 | Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a 3446 that avoids the existential quantifiers of copsexg 4956). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | csbopeq1a 7221 | Equality theorem for substitution of a class for an ordered pair in (analogue of csbeq1a 3542). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | dfopab2 7222* | A way to define an ordered-pair class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | dfoprab3s 7223* | A way to define an operation class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | dfoprab3 7224* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.) |
Theorem | dfoprab4 7225* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | dfoprab4f 7226* | Operation class abstraction expressed without existential quantifiers. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | opabex2 7227* | Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019.) |
Theorem | opabn1stprc 7228* | An ordered-pair class abstraction which does not depend on the first abstraction variable is a proper class. There must be, however, at least one set which satisfies the restricting wwf. (Contributed by AV, 27-Dec-2020.) |
Theorem | opiota 7229* | The property of a uniquely specified ordered pair. The proof uses properties of the description binder. (Contributed by Mario Carneiro, 21-May-2015.) |
Theorem | dfxp3 7230* | Define the Cartesian product of three classes. Compare df-xp 5120. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) |
Theorem | elopabi 7231* | A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.) |
Theorem | eloprabi 7232* | A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006.) (Revised by David Abernethy, 19-Jun-2012.) |
Theorem | mpt2mptsx 7233* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | mpt2mpts 7234* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.) |
Theorem | dmmpt2ssx 7235* | The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.) |
Theorem | fmpt2x 7236* | Functionality, domain and codomain of a class given by the "maps to" notation, where is not constant but depends on . (Contributed by NM, 29-Dec-2014.) |
Theorem | fmpt2 7237* | Functionality, domain and range of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.) |
Theorem | fnmpt2 7238* | Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.) |
Theorem | fnmpt2i 7239* | Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.) |
Theorem | dmmpt2 7240* | Domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.) |
Theorem | ovmpt2elrn 7241* | An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.) |
Theorem | dmmpt2ga 7242* | Domain of an operation given by the "maps to" notation, closed form of dmmpt2 7240. (Contributed by Alexander van der Vekens, 10-Feb-2019.) |
Theorem | dmmpt2g 7243* | Domain of an operation given by the "maps to" notation, closed form of dmmpt2 7240. Caution: This theorem is only valid in the very special case where the value of the mapping is a constant! (Contributed by Alexander van der Vekens, 1-Jun-2017.) (Prove shortened by AV, 10-Feb-2019.) |
Theorem | mpt2exxg 7244* | Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.) |
Theorem | mpt2exg 7245* | Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.) |
Theorem | mpt2exga 7246* | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by NM, 12-Sep-2011.) |
Theorem | mpt2ex 7247* | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by Mario Carneiro, 20-Dec-2013.) |
Theorem | mptmpt2opabbrd 7248* | The operation value of a function value of a collection of ordered pairs of elements related in two ways. (Contributed by Alexander van Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
Theorem | mptmpt2opabovd 7249* | The operation value of a function value of a collection of ordered pairs of related elements (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
Theorem | el2mpt2csbcl 7250* | If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021.) |
Theorem | el2mpt2cl 7251* | If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. Using implicit substitution. (Contributed by AV, 21-May-2021.) |
Theorem | fnmpt2ovd 7252* | A function with a Cartesian product as domain is a mapping with two arguments defined by its operation values. (Contributed by AV, 20-Feb-2019.) |
Theorem | offval22 7253* | The function operation expressed as a mapping, variation of offval2 6914. (Contributed by SO, 15-Jul-2018.) |
Theorem | brovpreldm 7254 | If a binary relation holds for the result of an operation, the operands are in the domain of the operation. (Contributed by AV, 31-Dec-2020.) |
Theorem | bropopvvv 7255* | If a binary relation holds for the result of an operation which is a result of an operation, the involved classes are sets. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Proof shortened by AV, 3-Jan-2021.) |
Theorem | bropfvvvvlem 7256* | Lemma for bropfvvvv 7257. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.) |
Theorem | bropfvvvv 7257* | If a binary relation holds for the result of an operation which is a function value, the involved classes are sets. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.) |
Theorem | ovmptss 7258* | If all the values of the mapping are subsets of a class , then so is any evaluation of the mapping. (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | relmpt2opab 7259* | Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 9-Feb-2015.) |
Theorem | fmpt2co 7260* | Composition of two functions. Variation of fmptco 6396 when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015.) |
Theorem | oprabco 7261* | Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 26-Sep-2015.) |
Theorem | oprab2co 7262* | Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by David Abernethy, 23-Apr-2013.) |
Theorem | df1st2 7263* | An alternate possible definition of the function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | df2nd2 7264* | An alternate possible definition of the function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | 1stconst 7265 | The mapping of a restriction of the function to a constant function. (Contributed by NM, 14-Dec-2008.) |
Theorem | 2ndconst 7266 | The mapping of a restriction of the function to a converse constant function. (Contributed by NM, 27-Mar-2008.) |
Theorem | dfmpt2 7267* | Alternate definition for the "maps to" notation df-mpt2 6655 (although it requires that be a set). (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Theorem | mpt2sn 7268* | An operation (in maps-to notation) on two singletons. (Contributed by AV, 4-Aug-2019.) |
Theorem | curry1 7269* | Composition with turns any binary operation with a constant first operand into a function of the second operand only. This transformation is called "currying." (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Dec-2014.) |
Theorem | curry1val 7270 | The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | curry1f 7271 | Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008.) |
Theorem | curry2 7272* | Composition with turns any binary operation with a constant second operand into a function of the first operand only. This transformation is called "currying." (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008.) |
Theorem | curry2f 7273 | Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.) |
Theorem | curry2val 7274 | The value of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.) |
Theorem | cnvf1olem 7275 | Lemma for cnvf1o 7276. (Contributed by Mario Carneiro, 27-Apr-2014.) |
Theorem | cnvf1o 7276* | Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014.) |
Theorem | fparlem1 7277 | Lemma for fpar 7281. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fparlem2 7278 | Lemma for fpar 7281. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fparlem3 7279* | Lemma for fpar 7281. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fparlem4 7280* | Lemma for fpar 7281. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fpar 7281* | Merge two functions in parallel. Use as the second argument of a composition with a (2-place) operation to build compound operations such as . (Contributed by NM, 17-Sep-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
Theorem | fsplit 7282 | A function that can be used to feed a common value to both operands of an operation. Use as the second argument of a composition with the function of fpar 7281 in order to build compound functions such as . (Contributed by NM, 17-Sep-2007.) |
Theorem | f2ndf 7283 | The (second member of an ordered pair) function restricted to a function is a function of into the codomain of . (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
Theorem | fo2ndf 7284 | The (second member of an ordered pair) function restricted to a function is a function of onto the range of . (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
Theorem | f1o2ndf1 7285 | The (second member of an ordered pair) function restricted to a one-to-one function is a one-to-one function of onto the range of . (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
Theorem | algrflem 7286 | Lemma for algrf 15286 and related theorems. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | frxp 7287* | A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) (Proof shortened by Wolf Lammen, 4-Oct-2014.) |
Theorem | xporderlem 7288* | Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.) |
Theorem | poxp 7289* | A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
Theorem | soxp 7290* | A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
Theorem | wexp 7291* | A lexicographical ordering of two well-ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
Theorem | fnwelem 7292* | Lemma for fnwe 7293. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
Theorem | fnwe 7293* | A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
Theorem | fnse 7294* | Condition for the well-order in fnwe 7293 to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015.) |
Se Se | ||
In this section, the support of functions is defined and corresponding theorems are provided. Since basic properties (see suppval 7297) are based on the Axiom of Union (usage of dmexg 7097), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression (see suppimacnv 7306). The theorems which are based on this representation and which are provided in previous sections could be moved into this section to have all related theorems in one section, although they do not depend on the Axiom of Union. This was possible because they are not used before. The current theorems differ from the original ones by requiring that the classes representing the "function" (or its "domain") and the "zero element" are sets. Actually, this does not cause any problem (until now). | ||
Syntax | csupp 7295 | Extend class definition to include the support of functions. |
supp | ||
Definition | df-supp 7296* | Define the support of a function against a "zero" value. According to Wikipedia ("Support (mathematics)", 31-Mar-2019, https://en.wikipedia.org/wiki/Support_(mathematics)) "In mathematics, the support of a real-valued function f is the subset of the domain containing those elements which are not mapped to zero." and "The notion of support also extends in a natural way to functions taking values in more general sets than R [the real numbers] and to other objects.". The following definition allows for such extensions, being applicable for any sets (which usually are functions) and any element (even not necessarily from the range of the function) regarded as "zero". (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
supp | ||
Theorem | suppval 7297* | The value of the operation constructing the support of a function. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
supp | ||
Theorem | supp0prc 7298 | The support of a class is empty if either the class or the "zero" is a proper class. . (Contributed by AV, 28-May-2019.) |
supp | ||
Theorem | suppvalbr 7299* | The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019.) |
supp | ||
Theorem | supp0 7300 | The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019.) |
supp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |