![]() |
Metamath
Proof Explorer Theorem List (p. 89 of 481) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | brecop2 8801 | Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis. (Contributed by NM, 13-Feb-1996.) (Revised by AV, 12-Jul-2022.) |
âĒ dom âž = (ðš à ðš) & âĒ ðŧ = ((ðš à ðš) / âž ) & âĒ ð â (ðŧ à ðŧ) & âĒ âĪ â (ðš à ðš) & âĒ ÂŽ â â ðš & âĒ dom + = (ðš à ðš) & âĒ (((ðī â ðš â§ ðĩ â ðš) â§ (ðķ â ðš â§ ð· â ðš)) â ([âĻðī, ðĩâĐ] âž ð [âĻðķ, ð·âĐ] âž â (ðī + ð·) âĪ (ðĩ + ðķ))) â âĒ ([âĻðī, ðĩâĐ] âž ð [âĻðķ, ð·âĐ] âž â (ðī + ð·) âĪ (ðĩ + ðķ)) | ||
Theorem | eroveu 8802* | Lemma for erov 8804 and eroprf 8805. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
âĒ ð― = (ðī / ð ) & âĒ ðū = (ðĩ / ð) & âĒ (ð â ð â ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) & âĒ (ð â ðķ â ð) & âĒ (ð â + :(ðī à ðĩ)âķðķ) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðĩ â§ ðĒ â ðĩ))) â ((ðð ð â§ ðĄððĒ) â (ð + ðĄ)ð(ð + ðĒ))) â âĒ ((ð â§ (ð â ð― â§ ð â ðū)) â â!ð§âð â ðī âð â ðĩ ((ð = [ð]ð â§ ð = [ð]ð) â§ ð§ = [(ð + ð)]ð)) | ||
Theorem | erovlem 8803* | Lemma for erov 8804 and eroprf 8805. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
âĒ ð― = (ðī / ð ) & âĒ ðū = (ðĩ / ð) & âĒ (ð â ð â ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) & âĒ (ð â ðķ â ð) & âĒ (ð â + :(ðī à ðĩ)âķðķ) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðĩ â§ ðĒ â ðĩ))) â ((ðð ð â§ ðĄððĒ) â (ð + ðĄ)ð(ð + ðĒ))) & âĒ âĻĢ = {âĻâĻðĨ, ðĶâĐ, ð§âĐ âĢ âð â ðī âð â ðĩ ((ðĨ = [ð]ð â§ ðĶ = [ð]ð) â§ ð§ = [(ð + ð)]ð)} â âĒ (ð â âĻĢ = (ðĨ â ð―, ðĶ â ðū âĶ (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð â§ ðĶ = [ð]ð) â§ ð§ = [(ð + ð)]ð)))) | ||
Theorem | erov 8804* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
âĒ ð― = (ðī / ð ) & âĒ ðū = (ðĩ / ð) & âĒ (ð â ð â ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) & âĒ (ð â ðķ â ð) & âĒ (ð â + :(ðī à ðĩ)âķðķ) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðĩ â§ ðĒ â ðĩ))) â ((ðð ð â§ ðĄððĒ) â (ð + ðĄ)ð(ð + ðĒ))) & âĒ âĻĢ = {âĻâĻðĨ, ðĶâĐ, ð§âĐ âĢ âð â ðī âð â ðĩ ((ðĨ = [ð]ð â§ ðĶ = [ð]ð) â§ ð§ = [(ð + ð)]ð)} & âĒ (ð â ð â ð) & âĒ (ð â ð â ð) â âĒ ((ð â§ ð â ðī â§ ð â ðĩ) â ([ð]ð âĻĢ [ð]ð) = [(ð + ð)]ð) | ||
Theorem | eroprf 8805* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
âĒ ð― = (ðī / ð ) & âĒ ðū = (ðĩ / ð) & âĒ (ð â ð â ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) & âĒ (ð â ðķ â ð) & âĒ (ð â + :(ðī à ðĩ)âķðķ) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðĩ â§ ðĒ â ðĩ))) â ((ðð ð â§ ðĄððĒ) â (ð + ðĄ)ð(ð + ðĒ))) & âĒ âĻĢ = {âĻâĻðĨ, ðĶâĐ, ð§âĐ âĢ âð â ðī âð â ðĩ ((ðĨ = [ð]ð â§ ðĶ = [ð]ð) â§ ð§ = [(ð + ð)]ð)} & âĒ (ð â ð â ð) & âĒ (ð â ð â ð) & âĒ ðŋ = (ðķ / ð) â âĒ (ð â âĻĢ :(ð― à ðū)âķðŋ) | ||
Theorem | erov2 8806* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
âĒ ð― = (ðī / âž ) & âĒ âĻĢ = {âĻâĻðĨ, ðĶâĐ, ð§âĐ âĢ âð â ðī âð â ðī ((ðĨ = [ð] âž â§ ðĶ = [ð] âž ) â§ ð§ = [(ð + ð)] âž )} & âĒ (ð â âž â ð) & âĒ (ð â âž Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â + :(ðī à ðī)âķðī) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðī â§ ðĒ â ðī))) â ((ð âž ð â§ ðĄ âž ðĒ) â (ð + ðĄ) âž (ð + ðĒ))) â âĒ ((ð â§ ð â ðī â§ ð â ðī) â ([ð] âž âĻĢ [ð] âž ) = [(ð + ð)] âž ) | ||
Theorem | eroprf2 8807* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
âĒ ð― = (ðī / âž ) & âĒ âĻĢ = {âĻâĻðĨ, ðĶâĐ, ð§âĐ âĢ âð â ðī âð â ðī ((ðĨ = [ð] âž â§ ðĶ = [ð] âž ) â§ ð§ = [(ð + ð)] âž )} & âĒ (ð â âž â ð) & âĒ (ð â âž Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â + :(ðī à ðī)âķðī) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðī â§ ðĒ â ðī))) â ((ð âž ð â§ ðĄ âž ðĒ) â (ð + ðĄ) âž (ð + ðĒ))) â âĒ (ð â âĻĢ :(ð― à ð―)âķð―) | ||
Theorem | ecopoveq 8808* | 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 8809* | 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 8810* | 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 8811* | 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.) |
âĒ âž = {âĻðĨ, ðĶâĐ âĢ ((ðĨ â (ð à ð) â§ ðĶ â (ð à ð)) â§ âð§âðĪâðĢâðĒ((ðĨ = âĻð§, ðĪâĐ â§ ðĶ = âĻðĢ, ðĒâĐ) â§ (ð§ + ðĒ) = (ðĪ + ðĢ)))} & âĒ (ðĨ + ðĶ) = (ðĶ + ðĨ) & âĒ ((ðĨ â ð â§ ðĶ â ð) â (ðĨ + ðĶ) â ð) & âĒ ((ðĨ + ðĶ) + ð§) = (ðĨ + (ðĶ + ð§)) & âĒ ((ðĨ â ð â§ ðĶ â ð) â ((ðĨ + ðĶ) = (ðĨ + ð§) â ðĶ = ð§)) â âĒ âž Er (ð à ð) | ||
Theorem | eceqoveq 8812* | Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) |
âĒ âž Er (ð à ð) & âĒ dom + = (ð à ð) & âĒ ÂŽ â â ð & âĒ ((ðĨ â ð â§ ðĶ â ð) â (ðĨ + ðĶ) â ð) & âĒ (((ðī â ð â§ ðĩ â ð) â§ (ðķ â ð â§ ð· â ð)) â (âĻðī, ðĩâĐ âž âĻðķ, ð·âĐ â (ðī + ð·) = (ðĩ + ðķ))) â âĒ ((ðī â ð â§ ðķ â ð) â ([âĻðī, ðĩâĐ] âž = [âĻðķ, ð·âĐ] âž â (ðī + ð·) = (ðĩ + ðķ))) | ||
Theorem | ecovcom 8813* | 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 8814* | 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 8815* | 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 8816 | Extend the definition of a class to include the mapping operation. (Read for ðī âm ðĩ, "the set of all functions that map from ðĩ to ðī.) |
class âm | ||
Syntax | cpm 8817 | Extend the definition of a class to include the partial mapping operation. (Read for ðī âpm ðĩ, "the set of all partial functions that map from ðĩ to ðī.) |
class âpm | ||
Definition | df-map 8818* | Define the mapping operation or set exponentiation. The set of all functions that map from ðĩ to ðī is written (ðī âm ðĩ) (see mapval 8828). 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 (ðī âm ðĩ). 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.) |
âĒ âm = (ðĨ â V, ðĶ â V âĶ {ð âĢ ð:ðĶâķðĨ}) | ||
Definition | df-pm 8819* | 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 (ðī âpm ðĩ) (see pmvalg 8827). A notation for this operation apparently does not appear in the literature. We use âpm to distinguish it from the less general set exponentiation operation âm (df-map 8818). See mapsspm 8866 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.) |
âĒ âpm = (ðĨ â V, ðĶ â V âĶ {ð â ðŦ (ðĶ Ã ðĨ) âĢ Fun ð}) | ||
Theorem | mapprc 8820* | 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.) |
âĒ (ÂŽ ðī â V â {ð âĢ ð:ðīâķðĩ} = â ) | ||
Theorem | pmex 8821* | The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.) |
âĒ ((ðī â ðķ â§ ðĩ â ð·) â {ð âĢ (Fun ð â§ ð â (ðī à ðĩ))} â V) | ||
Theorem | mapex 8822* | 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.) |
âĒ ((ðī â ðķ â§ ðĩ â ð·) â {ð âĢ ð:ðīâķðĩ} â V) | ||
Theorem | fnmap 8823 | Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.) |
âĒ âm Fn (V à V) | ||
Theorem | fnpm 8824 | Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.) |
âĒ âpm Fn (V à V) | ||
Theorem | reldmmap 8825 | Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
âĒ Rel dom âm | ||
Theorem | mapvalg 8826* | The value of set exponentiation. (ðī âm ðĩ) 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.) |
âĒ ((ðī â ðķ â§ ðĩ â ð·) â (ðī âm ðĩ) = {ð âĢ ð:ðĩâķðī}) | ||
Theorem | pmvalg 8827* | The value of the partial mapping operation. (ðī âpm ðĩ) is the set of all partial functions that map from ðĩ to ðī. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.) |
âĒ ((ðī â ðķ â§ ðĩ â ð·) â (ðī âpm ðĩ) = {ð â ðŦ (ðĩ à ðī) âĢ Fun ð}) | ||
Theorem | mapval 8828* | The value of set exponentiation (inference version). (ðī âm ðĩ) is the set of all functions that map from ðĩ to ðī. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ (ðī âm ðĩ) = {ð âĢ ð:ðĩâķðī} | ||
Theorem | elmapg 8829 | Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.) |
âĒ ((ðī â ð â§ ðĩ â ð) â (ðķ â (ðī âm ðĩ) â ðķ:ðĩâķðī)) | ||
Theorem | elmapd 8830 | Deduction form of elmapg 8829. (Contributed by BJ, 11-Apr-2020.) |
âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) â âĒ (ð â (ðķ â (ðī âm ðĩ) â ðķ:ðĩâķðī)) | ||
Theorem | elmapdd 8831 | Deduction associated with elmapd 8830. (Contributed by SN, 29-Jul-2024.) |
âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) & âĒ (ð â ðķ:ðĩâķðī) â âĒ (ð â ðķ â (ðī âm ðĩ)) | ||
Theorem | mapdm0 8832 | 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.) |
âĒ (ðĩ â ð â (ðĩ âm â ) = {â }) | ||
Theorem | elpmg 8833 | The predicate "is a partial function". (Contributed by Mario Carneiro, 14-Nov-2013.) |
âĒ ((ðī â ð â§ ðĩ â ð) â (ðķ â (ðī âpm ðĩ) â (Fun ðķ â§ ðķ â (ðĩ à ðī)))) | ||
Theorem | elpm2g 8834 | The predicate "is a partial function". (Contributed by NM, 31-Dec-2013.) |
âĒ ((ðī â ð â§ ðĩ â ð) â (ðđ â (ðī âpm ðĩ) â (ðđ:dom ðđâķðī â§ dom ðđ â ðĩ))) | ||
Theorem | elpm2r 8835 | Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013.) |
âĒ (((ðī â ð â§ ðĩ â ð) â§ (ðđ:ðķâķðī â§ ðķ â ðĩ)) â ðđ â (ðī âpm ðĩ)) | ||
Theorem | elpmi 8836 | A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
âĒ (ðđ â (ðī âpm ðĩ) â (ðđ:dom ðđâķðī â§ dom ðđ â ðĩ)) | ||
Theorem | pmfun 8837 | A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
âĒ (ðđ â (ðī âpm ðĩ) â Fun ðđ) | ||
Theorem | elmapex 8838 | Eliminate antecedent for mapping theorems: domain can be taken to be a set. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
âĒ (ðī â (ðĩ âm ðķ) â (ðĩ â V â§ ðķ â V)) | ||
Theorem | elmapi 8839 | A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
âĒ (ðī â (ðĩ âm ðķ) â ðī:ðķâķðĩ) | ||
Theorem | mapfset 8840* | If ðĩ is a set, the value of the set exponentiation (ðĩ âm ðī) is the class of all functions from ðī to ðĩ. Generalisation of mapvalg 8826 (which does not require ax-rep 5275) to arbitrary domains. Note that the class {ð âĢ ð:ðīâķðĩ} can only contain set-functions, as opposed to arbitrary class-functions. When ðī is a proper class, there can be no set-functions on it, so the above class is empty (see also fsetdmprc0 8845), hence a set. In this case, both sides of the equality in this theorem are the empty set. (Contributed by AV, 8-Aug-2024.) |
âĒ (ðĩ â ð â {ð âĢ ð:ðīâķðĩ} = (ðĩ âm ðī)) | ||
Theorem | mapssfset 8841* | The value of the set exponentiation (ðĩ âm ðī) is a subset of the class of functions from ðī to ðĩ. (Contributed by AV, 10-Aug-2024.) |
âĒ (ðĩ âm ðī) â {ð âĢ ð:ðīâķðĩ} | ||
Theorem | mapfoss 8842* | The value of the set exponentiation (ðĩ âm ðī) is a superset of the set of all functions from ðī onto ðĩ. (Contributed by AV, 7-Aug-2024.) |
âĒ {ð âĢ ð:ðīâontoâðĩ} â (ðĩ âm ðī) | ||
Theorem | fsetsspwxp 8843* | The class of all functions from ðī into ðĩ is a subclass of the power class of the cartesion product of ðī and ðĩ. (Contributed by AV, 13-Sep-2024.) |
âĒ {ð âĢ ð:ðīâķðĩ} â ðŦ (ðī à ðĩ) | ||
Theorem | fset0 8844 | The set of functions from the empty set is the singleton containing the empty set. (Contributed by AV, 13-Sep-2024.) |
âĒ {ð âĢ ð:â âķðĩ} = {â } | ||
Theorem | fsetdmprc0 8845* | The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024.) |
âĒ (ðī â V â {ð âĢ ð Fn ðī} = â ) | ||
Theorem | fsetex 8846* | The set of functions between two classes exists if the codomain exists. Generalization of mapex 8822 to arbitrary domains. (Contributed by AV, 14-Aug-2024.) |
âĒ (ðĩ â ð â {ð âĢ ð:ðīâķðĩ} â V) | ||
Theorem | f1setex 8847* | The set of injections between two classes exists if the codomain exists. (Contributed by AV, 14-Aug-2024.) |
âĒ (ðĩ â ð â {ð âĢ ð:ðīâ1-1âðĩ} â V) | ||
Theorem | fosetex 8848* | The set of surjections between two classes exists (without any precondition). (Contributed by AV, 8-Aug-2024.) |
âĒ {ð âĢ ð:ðīâontoâðĩ} â V | ||
Theorem | f1osetex 8849* | The set of bijections between two classes exists. (Contributed by AV, 30-Mar-2024.) (Revised by AV, 8-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.) |
âĒ {ð âĢ ð:ðīâ1-1-ontoâðĩ} â V | ||
Theorem | fsetfcdm 8850* | The class of functions with a given domain and a given codomain is mapped, through evaluation at a point of the domain, into the codomain. (Contributed by AV, 15-Sep-2024.) |
âĒ ðđ = {ð âĢ ð:ðīâķðĩ} & âĒ ð = (ð â ðđ âĶ (ðâð)) â âĒ (ð â ðī â ð:ðđâķðĩ) | ||
Theorem | fsetfocdm 8851* | The class of functions with a given domain that is a set and a given codomain is mapped, through evaluation at a point of the domain, onto the codomain. (Contributed by AV, 15-Sep-2024.) |
âĒ ðđ = {ð âĢ ð:ðīâķðĩ} & âĒ ð = (ð â ðđ âĶ (ðâð)) â âĒ ((ðī â ð â§ ð â ðī) â ð:ðđâontoâðĩ) | ||
Theorem | fsetprcnex 8852* | The class of all functions from a nonempty set ðī into a proper class ðĩ is not a set. If one of the preconditions is not fufilled, then {ð âĢ ð:ðīâķðĩ} is a set, see fsetdmprc0 8845 for ðī â V, fset0 8844 for ðī = â , and fsetex 8846 for ðĩ â V, see also fsetexb 8854. (Contributed by AV, 14-Sep-2024.) (Proof shortened by BJ, 15-Sep-2024.) |
âĒ (((ðī â ð â§ ðī â â ) â§ ðĩ â V) â {ð âĢ ð:ðīâķðĩ} â V) | ||
Theorem | fsetcdmex 8853* | The class of all functions from a nonempty set ðī into a class ðĩ is a set iff ðĩ is a set . (Contributed by AV, 15-Sep-2024.) |
âĒ ((ðī â ð â§ ðī â â ) â (ðĩ â V â {ð âĢ ð:ðīâķðĩ} â V)) | ||
Theorem | fsetexb 8854* | The class of all functions from a class ðī into a class ðĩ is a set iff ðĩ is a set or ðī is not a set or ðī is empty. (Contributed by AV, 15-Sep-2024.) |
âĒ ({ð âĢ ð:ðīâķðĩ} â V â (ðī â V âĻ ðī = â âĻ ðĩ â V)) | ||
Theorem | elmapfn 8855 | A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.) |
âĒ (ðī â (ðĩ âm ðķ) â ðī Fn ðķ) | ||
Theorem | elmapfun 8856 | A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
âĒ (ðī â (ðĩ âm ðķ) â Fun ðī) | ||
Theorem | elmapssres 8857 | A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.) |
âĒ ((ðī â (ðĩ âm ðķ) â§ ð· â ðķ) â (ðī âū ð·) â (ðĩ âm ð·)) | ||
Theorem | fpmg 8858 | A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
âĒ ((ðī â ð â§ ðĩ â ð â§ ðđ:ðīâķðĩ) â ðđ â (ðĩ âpm ðī)) | ||
Theorem | pmss12g 8859 | Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
âĒ (((ðī â ðķ â§ ðĩ â ð·) â§ (ðķ â ð â§ ð· â ð)) â (ðī âpm ðĩ) â (ðķ âpm ð·)) | ||
Theorem | pmresg 8860 | Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
âĒ ((ðĩ â ð â§ ðđ â (ðī âpm ðķ)) â (ðđ âū ðĩ) â (ðī âpm ðĩ)) | ||
Theorem | elmap 8861 | Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ (ðđ â (ðī âm ðĩ) â ðđ:ðĩâķðī) | ||
Theorem | mapval2 8862* | Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ (ðī âm ðĩ) = (ðŦ (ðĩ à ðī) âĐ {ð âĢ ð Fn ðĩ}) | ||
Theorem | elpm 8863 | The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ (ðđ â (ðī âpm ðĩ) â (Fun ðđ â§ ðđ â (ðĩ à ðī))) | ||
Theorem | elpm2 8864 | The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ (ðđ â (ðī âpm ðĩ) â (ðđ:dom ðđâķðī â§ dom ðđ â ðĩ)) | ||
Theorem | fpm 8865 | A total function is a partial function. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ (ðđ:ðīâķðĩ â ðđ â (ðĩ âpm ðī)) | ||
Theorem | mapsspm 8866 | Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.) |
âĒ (ðī âm ðĩ) â (ðī âpm ðĩ) | ||
Theorem | pmsspw 8867 | Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.) |
âĒ (ðī âpm ðĩ) â ðŦ (ðĩ à ðī) | ||
Theorem | mapsspw 8868 | 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.) |
âĒ (ðī âm ðĩ) â ðŦ (ðĩ à ðī) | ||
Theorem | mapfvd 8869 | The value of a function that maps from ðĩ to ðī. (Contributed by AV, 2-Feb-2023.) |
âĒ ð = (ðī âm ðĩ) & âĒ (ð â ðđ â ð) & âĒ (ð â ð â ðĩ) â âĒ (ð â (ðđâð) â ðī) | ||
Theorem | elmapresaun 8870 | fresaun 6752 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
âĒ ((ðđ â (ðķ âm ðī) â§ ðš â (ðķ âm ðĩ) â§ (ðđ âū (ðī âĐ ðĩ)) = (ðš âū (ðī âĐ ðĩ))) â (ðđ ⊠ðš) â (ðķ âm (ðī ⊠ðĩ))) | ||
Theorem | fvmptmap 8871* | Special case of fvmpt 6988 for operator theorems. (Contributed by NM, 27-Nov-2007.) |
âĒ ðķ â V & âĒ ð· â V & âĒ ð â V & âĒ (ðĨ = ðī â ðĩ = ðķ) & âĒ ðđ = (ðĨ â (ð âm ð·) âĶ ðĩ) â âĒ (ðī:ð·âķð â (ðđâðī) = ðķ) | ||
Theorem | map0e 8872 | 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.) (Proof shortened by AV, 14-Jul-2022.) |
âĒ (ðī â ð â (ðī âm â ) = 1o) | ||
Theorem | map0b 8873 | 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.) |
âĒ (ðī â â â (â âm ðī) = â ) | ||
Theorem | map0g 8874 | 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.) |
âĒ ((ðī â ð â§ ðĩ â ð) â ((ðī âm ðĩ) = â â (ðī = â â§ ðĩ â â ))) | ||
Theorem | 0map0sn0 8875 | The set of mappings of the empty set to the empty set is the singleton containing the empty set. (Contributed by AV, 31-Mar-2024.) |
âĒ (â âm â ) = {â } | ||
Theorem | mapsnd 8876* | The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Glauco Siliprandi, 24-Dec-2020.) |
âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) â âĒ (ð â (ðī âm {ðĩ}) = {ð âĢ âðĶ â ðī ð = {âĻðĩ, ðĶâĐ}}) | ||
Theorem | map0 8877 | 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.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ ((ðī âm ðĩ) = â â (ðī = â â§ ðĩ â â )) | ||
Theorem | mapsn 8878* | The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Proof shortened by AV, 17-Jul-2022.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ (ðī âm {ðĩ}) = {ð âĢ âðĶ â ðī ð = {âĻðĩ, ðĶâĐ}} | ||
Theorem | mapss 8879 | Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
âĒ ((ðĩ â ð â§ ðī â ðĩ) â (ðī âm ðķ) â (ðĩ âm ðķ)) | ||
Theorem | fdiagfn 8880* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
âĒ ðđ = (ðĨ â ðĩ âĶ (ðž à {ðĨ})) â âĒ ((ðĩ â ð â§ ðž â ð) â ðđ:ðĩâķ(ðĩ âm ðž)) | ||
Theorem | fvdiagfn 8881* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
âĒ ðđ = (ðĨ â ðĩ âĶ (ðž à {ðĨ})) â âĒ ((ðž â ð â§ ð â ðĩ) â (ðđâð) = (ðž à {ð})) | ||
Theorem | mapsnconst 8882 | Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
âĒ ð = {ð} & âĒ ðĩ â V & âĒ ð â V â âĒ (ðđ â (ðĩ âm ð) â ðđ = (ð à {(ðđâð)})) | ||
Theorem | mapsncnv 8883* | Expression for the inverse of the canonical map between a set and its set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
âĒ ð = {ð} & âĒ ðĩ â V & âĒ ð â V & âĒ ðđ = (ðĨ â (ðĩ âm ð) âĶ (ðĨâð)) â âĒ âĄðđ = (ðĶ â ðĩ âĶ (ð à {ðĶ})) | ||
Theorem | mapsnf1o2 8884* | Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
âĒ ð = {ð} & âĒ ðĩ â V & âĒ ð â V & âĒ ðđ = (ðĨ â (ðĩ âm ð) âĶ (ðĨâð)) â âĒ ðđ:(ðĩ âm ð)â1-1-ontoâðĩ | ||
Theorem | mapsnf1o3 8885* | Explicit bijection in the reverse of mapsnf1o2 8884. (Contributed by Stefan O'Rear, 24-Mar-2015.) |
âĒ ð = {ð} & âĒ ðĩ â V & âĒ ð â V & âĒ ðđ = (ðĶ â ðĩ âĶ (ð à {ðĶ})) â âĒ ðđ:ðĩâ1-1-ontoâ(ðĩ âm ð) | ||
Theorem | ralxpmap 8886* | Quantification over functions in terms of quantification over values and punctured functions. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.) |
âĒ (ð = (ð ⊠{âĻð―, ðĶâĐ}) â (ð â ð)) â âĒ (ð― â ð â (âð â (ð âm ð)ð â âðĶ â ð âð â (ð âm (ð â {ð―}))ð)) | ||
Syntax | cixp 8887 | Extend class notation to include infinite Cartesian products. |
class XðĨ â ðī ðĩ | ||
Definition | df-ixp 8888* | Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with ðĨ â ðī written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually ðĩ represents a class expression containing ðĨ free and thus can be thought of as ðĩ(ðĨ). Normally, ðĨ is not free in ðī, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.) |
âĒ XðĨ â ðī ðĩ = {ð âĢ (ð Fn {ðĨ âĢ ðĨ â ðī} â§ âðĨ â ðī (ðâðĨ) â ðĩ)} | ||
Theorem | dfixp 8889* | Eliminate the expression {ðĨ âĢ ðĨ â ðī} in df-ixp 8888, under the assumption that ðī and ðĨ are disjoint. This way, we can say that ðĨ is bound in XðĨ â ðīðĩ even if it appears free in ðī. (Contributed by Mario Carneiro, 12-Aug-2016.) |
âĒ XðĨ â ðī ðĩ = {ð âĢ (ð Fn ðī â§ âðĨ â ðī (ðâðĨ) â ðĩ)} | ||
Theorem | ixpsnval 8890* | The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.) |
âĒ (ð â ð â XðĨ â {ð}ðĩ = {ð âĢ (ð Fn {ð} â§ (ðâð) â âĶð / ðĨâĶðĩ)}) | ||
Theorem | elixp2 8891* | Membership in an infinite Cartesian product. See df-ixp 8888 for discussion of the notation. (Contributed by NM, 28-Sep-2006.) |
âĒ (ðđ â XðĨ â ðī ðĩ â (ðđ â V â§ ðđ Fn ðī â§ âðĨ â ðī (ðđâðĨ) â ðĩ)) | ||
Theorem | fvixp 8892* | Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
âĒ (ðĨ = ðķ â ðĩ = ð·) â âĒ ((ðđ â XðĨ â ðī ðĩ â§ ðķ â ðī) â (ðđâðķ) â ð·) | ||
Theorem | ixpfn 8893* | A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.) |
âĒ (ðđ â XðĨ â ðī ðĩ â ðđ Fn ðī) | ||
Theorem | elixp 8894* | Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.) |
âĒ ðđ â V â âĒ (ðđ â XðĨ â ðī ðĩ â (ðđ Fn ðī â§ âðĨ â ðī (ðđâðĨ) â ðĩ)) | ||
Theorem | elixpconst 8895* | Membership in an infinite Cartesian product of a constant ðĩ. (Contributed by NM, 12-Apr-2008.) |
âĒ ðđ â V â âĒ (ðđ â XðĨ â ðī ðĩ â ðđ:ðīâķðĩ) | ||
Theorem | ixpconstg 8896* | Infinite Cartesian product of a constant ðĩ. (Contributed by Mario Carneiro, 11-Jan-2015.) |
âĒ ((ðī â ð â§ ðĩ â ð) â XðĨ â ðī ðĩ = (ðĩ âm ðī)) | ||
Theorem | ixpconst 8897* | Infinite Cartesian product of a constant ðĩ. (Contributed by NM, 28-Sep-2006.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ XðĨ â ðī ðĩ = (ðĩ âm ðī) | ||
Theorem | ixpeq1 8898* | Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) |
âĒ (ðī = ðĩ â XðĨ â ðī ðķ = XðĨ â ðĩ ðķ) | ||
Theorem | ixpeq1d 8899* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
âĒ (ð â ðī = ðĩ) â âĒ (ð â XðĨ â ðī ðķ = XðĨ â ðĩ ðķ) | ||
Theorem | ss2ixp 8900 | Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.) |
âĒ (âðĨ â ðī ðĩ â ðķ â XðĨ â ðī ðĩ â XðĨ â ðī ðķ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |