![]() |
Metamath
Proof Explorer Theorem List (p. 89 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | qliftf 8801* | The domain and codomain of the function ðđ. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
âĒ ðđ = ran (ðĨ â ð âĶ âĻ[ðĨ]ð , ðīâĐ) & âĒ ((ð â§ ðĨ â ð) â ðī â ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð â ð) â âĒ (ð â (Fun ðđ â ðđ:(ð / ð )âķð)) | ||
Theorem | qliftval 8802* | The value of the function ðđ. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
âĒ ðđ = ran (ðĨ â ð âĶ âĻ[ðĨ]ð , ðīâĐ) & âĒ ((ð â§ ðĨ â ð) â ðī â ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð â ð) & âĒ (ðĨ = ðķ â ðī = ðĩ) & âĒ (ð â Fun ðđ) â âĒ ((ð â§ ðķ â ð) â (ðđâ[ðķ]ð ) = ðĩ) | ||
Theorem | ecoptocl 8803* | Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.) |
âĒ ð = ((ðĩ à ðķ) / ð ) & âĒ ([âĻðĨ, ðĶâĐ]ð = ðī â (ð â ð)) & âĒ ((ðĨ â ðĩ â§ ðĶ â ðķ) â ð) â âĒ (ðī â ð â ð) | ||
Theorem | 2ecoptocl 8804* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.) |
âĒ ð = ((ðķ à ð·) / ð ) & âĒ ([âĻðĨ, ðĶâĐ]ð = ðī â (ð â ð)) & âĒ ([âĻð§, ðĪâĐ]ð = ðĩ â (ð â ð)) & âĒ (((ðĨ â ðķ â§ ðĶ â ð·) â§ (ð§ â ðķ â§ ðĪ â ð·)) â ð) â âĒ ((ðī â ð â§ ðĩ â ð) â ð) | ||
Theorem | 3ecoptocl 8805* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.) |
âĒ ð = ((ð· à ð·) / ð ) & âĒ ([âĻðĨ, ðĶâĐ]ð = ðī â (ð â ð)) & âĒ ([âĻð§, ðĪâĐ]ð = ðĩ â (ð â ð)) & âĒ ([âĻðĢ, ðĒâĐ]ð = ðķ â (ð â ð)) & âĒ (((ðĨ â ð· â§ ðĶ â ð·) â§ (ð§ â ð· â§ ðĪ â ð·) â§ (ðĢ â ð· â§ ðĒ â ð·)) â ð) â âĒ ((ðī â ð â§ ðĩ â ð â§ ðķ â ð) â ð) | ||
Theorem | brecop 8806* | Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.) |
âĒ âž â V & âĒ âž Er (ðš à ðš) & âĒ ðŧ = ((ðš à ðš) / âž ) & âĒ âĪ = {âĻðĨ, ðĶâĐ âĢ ((ðĨ â ðŧ â§ ðĶ â ðŧ) â§ âð§âðĪâðĢâðĒ((ðĨ = [âĻð§, ðĪâĐ] âž â§ ðĶ = [âĻðĢ, ðĒâĐ] âž ) â§ ð))} & âĒ ((((ð§ â ðš â§ ðĪ â ðš) â§ (ðī â ðš â§ ðĩ â ðš)) â§ ((ðĢ â ðš â§ ðĒ â ðš) â§ (ðķ â ðš â§ ð· â ðš))) â (([âĻð§, ðĪâĐ] âž = [âĻðī, ðĩâĐ] âž â§ [âĻðĢ, ðĒâĐ] âž = [âĻðķ, ð·âĐ] âž ) â (ð â ð))) â âĒ (((ðī â ðš â§ ðĩ â ðš) â§ (ðķ â ðš â§ ð· â ðš)) â ([âĻðī, ðĩâĐ] âž âĪ [âĻðķ, ð·âĐ] âž â ð)) | ||
Theorem | brecop2 8807 | 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 8808* | Lemma for erov 8810 and eroprf 8811. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
âĒ ð― = (ðī / ð ) & âĒ ðū = (ðĩ / ð) & âĒ (ð â ð â ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) & âĒ (ð â ðķ â ð) & âĒ (ð â + :(ðī à ðĩ)âķðķ) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðĩ â§ ðĒ â ðĩ))) â ((ðð ð â§ ðĄððĒ) â (ð + ðĄ)ð(ð + ðĒ))) â âĒ ((ð â§ (ð â ð― â§ ð â ðū)) â â!ð§âð â ðī âð â ðĩ ((ð = [ð]ð â§ ð = [ð]ð) â§ ð§ = [(ð + ð)]ð)) | ||
Theorem | erovlem 8809* | Lemma for erov 8810 and eroprf 8811. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
âĒ ð― = (ðī / ð ) & âĒ ðū = (ðĩ / ð) & âĒ (ð â ð â ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ð Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) & âĒ (ð â ðķ â ð) & âĒ (ð â + :(ðī à ðĩ)âķðķ) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðĩ â§ ðĒ â ðĩ))) â ((ðð ð â§ ðĄððĒ) â (ð + ðĄ)ð(ð + ðĒ))) & âĒ âĻĢ = {âĻâĻðĨ, ðĶâĐ, ð§âĐ âĢ âð â ðī âð â ðĩ ((ðĨ = [ð]ð â§ ðĶ = [ð]ð) â§ ð§ = [(ð + ð)]ð)} â âĒ (ð â âĻĢ = (ðĨ â ð―, ðĶ â ðū âĶ (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð â§ ðĶ = [ð]ð) â§ ð§ = [(ð + ð)]ð)))) | ||
Theorem | erov 8810* | 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 8811* | 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 8812* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
âĒ ð― = (ðī / âž ) & âĒ âĻĢ = {âĻâĻðĨ, ðĶâĐ, ð§âĐ âĢ âð â ðī âð â ðī ((ðĨ = [ð] âž â§ ðĶ = [ð] âž ) â§ ð§ = [(ð + ð)] âž )} & âĒ (ð â âž â ð) & âĒ (ð â âž Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â + :(ðī à ðī)âķðī) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðī â§ ðĒ â ðī))) â ((ð âž ð â§ ðĄ âž ðĒ) â (ð + ðĄ) âž (ð + ðĒ))) â âĒ ((ð â§ ð â ðī â§ ð â ðī) â ([ð] âž âĻĢ [ð] âž ) = [(ð + ð)] âž ) | ||
Theorem | eroprf2 8813* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
âĒ ð― = (ðī / âž ) & âĒ âĻĢ = {âĻâĻðĨ, ðĶâĐ, ð§âĐ âĢ âð â ðī âð â ðī ((ðĨ = [ð] âž â§ ðĶ = [ð] âž ) â§ ð§ = [(ð + ð)] âž )} & âĒ (ð â âž â ð) & âĒ (ð â âž Er ð) & âĒ (ð â ðī â ð) & âĒ (ð â + :(ðī à ðī)âķðī) & âĒ ((ð â§ ((ð â ðī â§ ð â ðī) â§ (ðĄ â ðī â§ ðĒ â ðī))) â ((ð âž ð â§ ðĄ âž ðĒ) â (ð + ðĄ) âž (ð + ðĒ))) â âĒ (ð â âĻĢ :(ð― à ð―)âķð―) | ||
Theorem | ecopoveq 8814* | 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 8815* | 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 8816* | 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 8817* | 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 8818* | 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 8819* | 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 8820* | 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 8821* | 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 8822 | 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 8823 | 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 8824* | Define the mapping operation or set exponentiation. The set of all functions that map from ðĩ to ðī is written (ðī âm ðĩ) (see mapval 8834). 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 8825* | 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 8833). 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 8824). See mapsspm 8872 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.) |
âĒ âpm = (ðĨ â V, ðĶ â V âĶ {ð â ðŦ (ðĶ Ã ðĨ) âĢ Fun ð}) | ||
Theorem | mapprc 8826* | 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 8827* | The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.) |
âĒ ((ðī â ðķ â§ ðĩ â ð·) â {ð âĢ (Fun ð â§ ð â (ðī à ðĩ))} â V) | ||
Theorem | mapex 8828* | 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 8829 | 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 8830 | Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.) |
âĒ âpm Fn (V à V) | ||
Theorem | reldmmap 8831 | Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
âĒ Rel dom âm | ||
Theorem | mapvalg 8832* | 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 8833* | 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 8834* | 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 8835 | Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.) |
âĒ ((ðī â ð â§ ðĩ â ð) â (ðķ â (ðī âm ðĩ) â ðķ:ðĩâķðī)) | ||
Theorem | elmapd 8836 | Deduction form of elmapg 8835. (Contributed by BJ, 11-Apr-2020.) |
âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) â âĒ (ð â (ðķ â (ðī âm ðĩ) â ðķ:ðĩâķðī)) | ||
Theorem | elmapdd 8837 | Deduction associated with elmapd 8836. (Contributed by SN, 29-Jul-2024.) |
âĒ (ð â ðī â ð) & âĒ (ð â ðĩ â ð) & âĒ (ð â ðķ:ðĩâķðī) â âĒ (ð â ðķ â (ðī âm ðĩ)) | ||
Theorem | mapdm0 8838 | 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 8839 | The predicate "is a partial function". (Contributed by Mario Carneiro, 14-Nov-2013.) |
âĒ ((ðī â ð â§ ðĩ â ð) â (ðķ â (ðī âpm ðĩ) â (Fun ðķ â§ ðķ â (ðĩ à ðī)))) | ||
Theorem | elpm2g 8840 | The predicate "is a partial function". (Contributed by NM, 31-Dec-2013.) |
âĒ ((ðī â ð â§ ðĩ â ð) â (ðđ â (ðī âpm ðĩ) â (ðđ:dom ðđâķðī â§ dom ðđ â ðĩ))) | ||
Theorem | elpm2r 8841 | Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013.) |
âĒ (((ðī â ð â§ ðĩ â ð) â§ (ðđ:ðķâķðī â§ ðķ â ðĩ)) â ðđ â (ðī âpm ðĩ)) | ||
Theorem | elpmi 8842 | A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
âĒ (ðđ â (ðī âpm ðĩ) â (ðđ:dom ðđâķðī â§ dom ðđ â ðĩ)) | ||
Theorem | pmfun 8843 | A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
âĒ (ðđ â (ðī âpm ðĩ) â Fun ðđ) | ||
Theorem | elmapex 8844 | 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 8845 | A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
âĒ (ðī â (ðĩ âm ðķ) â ðī:ðķâķðĩ) | ||
Theorem | mapfset 8846* | If ðĩ is a set, the value of the set exponentiation (ðĩ âm ðī) is the class of all functions from ðī to ðĩ. Generalisation of mapvalg 8832 (which does not require ax-rep 5284) 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 8851), 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 8847* | 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 8848* | 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 8849* | 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 8850 | The set of functions from the empty set is the singleton containing the empty set. (Contributed by AV, 13-Sep-2024.) |
âĒ {ð âĢ ð:â âķðĩ} = {â } | ||
Theorem | fsetdmprc0 8851* | The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024.) |
âĒ (ðī â V â {ð âĢ ð Fn ðī} = â ) | ||
Theorem | fsetex 8852* | The set of functions between two classes exists if the codomain exists. Generalization of mapex 8828 to arbitrary domains. (Contributed by AV, 14-Aug-2024.) |
âĒ (ðĩ â ð â {ð âĢ ð:ðīâķðĩ} â V) | ||
Theorem | f1setex 8853* | The set of injections between two classes exists if the codomain exists. (Contributed by AV, 14-Aug-2024.) |
âĒ (ðĩ â ð â {ð âĢ ð:ðīâ1-1âðĩ} â V) | ||
Theorem | fosetex 8854* | The set of surjections between two classes exists (without any precondition). (Contributed by AV, 8-Aug-2024.) |
âĒ {ð âĢ ð:ðīâontoâðĩ} â V | ||
Theorem | f1osetex 8855* | 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 8856* | 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 8857* | 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 8858* | 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 8851 for ðī â V, fset0 8850 for ðī = â , and fsetex 8852 for ðĩ â V, see also fsetexb 8860. (Contributed by AV, 14-Sep-2024.) (Proof shortened by BJ, 15-Sep-2024.) |
âĒ (((ðī â ð â§ ðī â â ) â§ ðĩ â V) â {ð âĢ ð:ðīâķðĩ} â V) | ||
Theorem | fsetcdmex 8859* | 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 8860* | 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 8861 | A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.) |
âĒ (ðī â (ðĩ âm ðķ) â ðī Fn ðķ) | ||
Theorem | elmapfun 8862 | 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 8863 | 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 8864 | A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
âĒ ((ðī â ð â§ ðĩ â ð â§ ðđ:ðīâķðĩ) â ðđ â (ðĩ âpm ðī)) | ||
Theorem | pmss12g 8865 | Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
âĒ (((ðī â ðķ â§ ðĩ â ð·) â§ (ðķ â ð â§ ð· â ð)) â (ðī âpm ðĩ) â (ðķ âpm ð·)) | ||
Theorem | pmresg 8866 | Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
âĒ ((ðĩ â ð â§ ðđ â (ðī âpm ðķ)) â (ðđ âū ðĩ) â (ðī âpm ðĩ)) | ||
Theorem | elmap 8867 | Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ (ðđ â (ðī âm ðĩ) â ðđ:ðĩâķðī) | ||
Theorem | mapval2 8868* | Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.) |
âĒ ðī â V & âĒ ðĩ â V â âĒ (ðī âm ðĩ) = (ðŦ (ðĩ à ðī) âĐ {ð âĢ ð Fn ðĩ}) | ||
Theorem | elpm 8869 | 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 8870 | 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 8871 | 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 8872 | 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 8873 | 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 8874 | 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 8875 | The value of a function that maps from ðĩ to ðī. (Contributed by AV, 2-Feb-2023.) |
âĒ ð = (ðī âm ðĩ) & âĒ (ð â ðđ â ð) & âĒ (ð â ð â ðĩ) â âĒ (ð â (ðđâð) â ðī) | ||
Theorem | elmapresaun 8876 | fresaun 6761 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
âĒ ((ðđ â (ðķ âm ðī) â§ ðš â (ðķ âm ðĩ) â§ (ðđ âū (ðī âĐ ðĩ)) = (ðš âū (ðī âĐ ðĩ))) â (ðđ ⊠ðš) â (ðķ âm (ðī ⊠ðĩ))) | ||
Theorem | fvmptmap 8877* | Special case of fvmpt 6997 for operator theorems. (Contributed by NM, 27-Nov-2007.) |
âĒ ðķ â V & âĒ ð· â V & âĒ ð â V & âĒ (ðĨ = ðī â ðĩ = ðķ) & âĒ ðđ = (ðĨ â (ð âm ð·) âĶ ðĩ) â âĒ (ðī:ð·âķð â (ðđâðī) = ðķ) | ||
Theorem | map0e 8878 | 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 8879 | 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 8880 | 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 8881 | 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 8882* | 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 8883 | 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 8884* | 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 8885 | 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 8886* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
âĒ ðđ = (ðĨ â ðĩ âĶ (ðž à {ðĨ})) â âĒ ((ðĩ â ð â§ ðž â ð) â ðđ:ðĩâķ(ðĩ âm ðž)) | ||
Theorem | fvdiagfn 8887* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
âĒ ðđ = (ðĨ â ðĩ âĶ (ðž à {ðĨ})) â âĒ ((ðž â ð â§ ð â ðĩ) â (ðđâð) = (ðž à {ð})) | ||
Theorem | mapsnconst 8888 | Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
âĒ ð = {ð} & âĒ ðĩ â V & âĒ ð â V â âĒ (ðđ â (ðĩ âm ð) â ðđ = (ð à {(ðđâð)})) | ||
Theorem | mapsncnv 8889* | 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 8890* | 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 8891* | Explicit bijection in the reverse of mapsnf1o2 8890. (Contributed by Stefan O'Rear, 24-Mar-2015.) |
âĒ ð = {ð} & âĒ ðĩ â V & âĒ ð â V & âĒ ðđ = (ðĶ â ðĩ âĶ (ð à {ðĶ})) â âĒ ðđ:ðĩâ1-1-ontoâ(ðĩ âm ð) | ||
Theorem | ralxpmap 8892* | 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 8893 | Extend class notation to include infinite Cartesian products. |
class XðĨ â ðī ðĩ | ||
Definition | df-ixp 8894* | 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 8895* | Eliminate the expression {ðĨ âĢ ðĨ â ðī} in df-ixp 8894, 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 8896* | The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.) |
âĒ (ð â ð â XðĨ â {ð}ðĩ = {ð âĢ (ð Fn {ð} â§ (ðâð) â âĶð / ðĨâĶðĩ)}) | ||
Theorem | elixp2 8897* | Membership in an infinite Cartesian product. See df-ixp 8894 for discussion of the notation. (Contributed by NM, 28-Sep-2006.) |
âĒ (ðđ â XðĨ â ðī ðĩ â (ðđ â V â§ ðđ Fn ðī â§ âðĨ â ðī (ðđâðĨ) â ðĩ)) | ||
Theorem | fvixp 8898* | Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
âĒ (ðĨ = ðķ â ðĩ = ð·) â âĒ ((ðđ â XðĨ â ðī ðĩ â§ ðķ â ðī) â (ðđâðķ) â ð·) | ||
Theorem | ixpfn 8899* | A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.) |
âĒ (ðđ â XðĨ â ðī ðĩ â ðđ Fn ðī) | ||
Theorem | elixp 8900* | Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.) |
âĒ ðđ â V â âĒ (ðđ â XðĨ â ðī ðĩ â (ðđ Fn ðī â§ âðĨ â ðī (ðđâðĨ) â ðĩ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |