![]() |
Intuitionistic Logic Explorer Theorem List (p. 63 of 151) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sbcopeq1a 6201 | Equality theorem for substitution of a class for an ordered pair (analog of sbceq1a 2984 that avoids the existential quantifiers of copsexg 4256). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
β’ (π΄ = β¨π₯, π¦β© β ([(1st βπ΄) / π₯][(2nd βπ΄) / π¦]π β π)) | ||
Theorem | csbopeq1a 6202 | Equality theorem for substitution of a class π΄ for an ordered pair β¨π₯, π¦β© in π΅ (analog of csbeq1a 3078). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
β’ (π΄ = β¨π₯, π¦β© β β¦(1st βπ΄) / π₯β¦β¦(2nd βπ΄) / π¦β¦π΅ = π΅) | ||
Theorem | dfopab2 6203* | 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.) |
β’ {β¨π₯, π¦β© β£ π} = {π§ β (V Γ V) β£ [(1st βπ§) / π₯][(2nd βπ§) / π¦]π} | ||
Theorem | dfoprab3s 6204* | 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.) |
β’ {β¨β¨π₯, π¦β©, π§β© β£ π} = {β¨π€, π§β© β£ (π€ β (V Γ V) β§ [(1st βπ€) / π₯][(2nd βπ€) / π¦]π)} | ||
Theorem | dfoprab3 6205* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.) |
β’ (π€ = β¨π₯, π¦β© β (π β π)) β β’ {β¨π€, π§β© β£ (π€ β (V Γ V) β§ π)} = {β¨β¨π₯, π¦β©, π§β© β£ π} | ||
Theorem | dfoprab4 6206* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
β’ (π€ = β¨π₯, π¦β© β (π β π)) β β’ {β¨π€, π§β© β£ (π€ β (π΄ Γ π΅) β§ π)} = {β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β π΄ β§ π¦ β π΅) β§ π)} | ||
Theorem | dfoprab4f 6207* | 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 | dfxp3 6208* | Define the cross product of three classes. Compare df-xp 4644. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) |
β’ ((π΄ Γ π΅) Γ πΆ) = {β¨β¨π₯, π¦β©, π§β© β£ (π₯ β π΄ β§ π¦ β π΅ β§ π§ β πΆ)} | ||
Theorem | elopabi 6209* | A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.) |
β’ (π₯ = (1st βπ΄) β (π β π)) & β’ (π¦ = (2nd βπ΄) β (π β π)) β β’ (π΄ β {β¨π₯, π¦β© β£ π} β π) | ||
Theorem | eloprabi 6210* | 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.) |
β’ (π₯ = (1st β(1st βπ΄)) β (π β π)) & β’ (π¦ = (2nd β(1st βπ΄)) β (π β π)) & β’ (π§ = (2nd βπ΄) β (π β π)) β β’ (π΄ β {β¨β¨π₯, π¦β©, π§β© β£ π} β π) | ||
Theorem | mpomptsx 6211* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = (π§ β βͺ π₯ β π΄ ({π₯} Γ π΅) β¦ β¦(1st βπ§) / π₯β¦β¦(2nd βπ§) / π¦β¦πΆ) | ||
Theorem | mpompts 6212* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.) |
β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = (π§ β (π΄ Γ π΅) β¦ β¦(1st βπ§) / π₯β¦β¦(2nd βπ§) / π¦β¦πΆ) | ||
Theorem | dmmpossx 6213* | The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ dom πΉ β βͺ π₯ β π΄ ({π₯} Γ π΅) | ||
Theorem | fmpox 6214* | 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 | fmpo 6215* | Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ (βπ₯ β π΄ βπ¦ β π΅ πΆ β π· β πΉ:(π΄ Γ π΅)βΆπ·) | ||
Theorem | fnmpo 6216* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ (βπ₯ β π΄ βπ¦ β π΅ πΆ β π β πΉ Fn (π΄ Γ π΅)) | ||
Theorem | mpofvex 6217* | Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ ((βπ₯βπ¦ πΆ β π β§ π β π β§ π β π) β (π πΉπ) β V) | ||
Theorem | fnmpoi 6218* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) & β’ πΆ β V β β’ πΉ Fn (π΄ Γ π΅) | ||
Theorem | dmmpo 6219* | Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) & β’ πΆ β V β β’ dom πΉ = (π΄ Γ π΅) | ||
Theorem | mpofvexi 6220* | Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) & β’ πΆ β V & β’ π β V & β’ π β V β β’ (π πΉπ) β V | ||
Theorem | ovmpoelrn 6221* | An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.) |
β’ π = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ ((βπ₯ β π΄ βπ¦ β π΅ πΆ β π β§ π β π΄ β§ π β π΅) β (πππ) β π) | ||
Theorem | dmmpoga 6222* | Domain of an operation given by the maps-to notation, closed form of dmmpo 6219. (Contributed by Alexander van der Vekens, 10-Feb-2019.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ (βπ₯ β π΄ βπ¦ β π΅ πΆ β π β dom πΉ = (π΄ Γ π΅)) | ||
Theorem | dmmpog 6223* | Domain of an operation given by the maps-to notation, closed form of dmmpo 6219. 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.) (Proof shortened by AV, 10-Feb-2019.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ (πΆ β π β dom πΉ = (π΄ Γ π΅)) | ||
Theorem | mpoexxg 6224* | Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ ((π΄ β π β§ βπ₯ β π΄ π΅ β π) β πΉ β V) | ||
Theorem | mpoexg 6225* | Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ ((π΄ β π β§ π΅ β π) β πΉ β V) | ||
Theorem | mpoexga 6226* | If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by NM, 12-Sep-2011.) |
β’ ((π΄ β π β§ π΅ β π) β (π₯ β π΄, π¦ β π΅ β¦ πΆ) β V) | ||
Theorem | mpoexw 6227* | Weak version of mpoex 6228 that holds without ax-coll 4130. If the domain and codomain of an operation given by maps-to notation are sets, the operation is a set. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ π΄ β V & β’ π΅ β V & β’ π· β V & β’ βπ₯ β π΄ βπ¦ β π΅ πΆ β π· β β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) β V | ||
Theorem | mpoex 6228* | If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013.) |
β’ π΄ β V & β’ π΅ β V β β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) β V | ||
Theorem | fnmpoovd 6229* | 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.) (Revised by AV, 3-Jul-2022.) |
β’ (π β π Fn (π΄ Γ π΅)) & β’ ((π = π β§ π = π) β π· = πΆ) & β’ ((π β§ π β π΄ β§ π β π΅) β π· β π) & β’ ((π β§ π β π΄ β§ π β π΅) β πΆ β π) β β’ (π β (π = (π β π΄, π β π΅ β¦ πΆ) β βπ β π΄ βπ β π΅ (πππ) = π·)) | ||
Theorem | fmpoco 6230* | Composition of two functions. Variation of fmptco 5695 when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΅)) β π β πΆ) & β’ (π β πΉ = (π₯ β π΄, π¦ β π΅ β¦ π )) & β’ (π β πΊ = (π§ β πΆ β¦ π)) & β’ (π§ = π β π = π) β β’ (π β (πΊ β πΉ) = (π₯ β π΄, π¦ β π΅ β¦ π)) | ||
Theorem | oprabco 6231* | Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 26-Sep-2015.) |
β’ ((π₯ β π΄ β§ π¦ β π΅) β πΆ β π·) & β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) & β’ πΊ = (π₯ β π΄, π¦ β π΅ β¦ (π»βπΆ)) β β’ (π» Fn π· β πΊ = (π» β πΉ)) | ||
Theorem | oprab2co 6232* | Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by David Abernethy, 23-Apr-2013.) |
β’ ((π₯ β π΄ β§ π¦ β π΅) β πΆ β π ) & β’ ((π₯ β π΄ β§ π¦ β π΅) β π· β π) & β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ β¨πΆ, π·β©) & β’ πΊ = (π₯ β π΄, π¦ β π΅ β¦ (πΆππ·)) β β’ (π Fn (π Γ π) β πΊ = (π β πΉ)) | ||
Theorem | df1st2 6233* | An alternate possible definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
β’ {β¨β¨π₯, π¦β©, π§β© β£ π§ = π₯} = (1st βΎ (V Γ V)) | ||
Theorem | df2nd2 6234* | An alternate possible definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
β’ {β¨β¨π₯, π¦β©, π§β© β£ π§ = π¦} = (2nd βΎ (V Γ V)) | ||
Theorem | 1stconst 6235 | The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008.) |
β’ (π΅ β π β (1st βΎ (π΄ Γ {π΅})):(π΄ Γ {π΅})β1-1-ontoβπ΄) | ||
Theorem | 2ndconst 6236 | The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008.) |
β’ (π΄ β π β (2nd βΎ ({π΄} Γ π΅)):({π΄} Γ π΅)β1-1-ontoβπ΅) | ||
Theorem | dfmpo 6237* | Alternate definition for the maps-to notation df-mpo 5893 (although it requires that πΆ be a set). (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.) |
β’ πΆ β V β β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = βͺ π₯ β π΄ βͺ π¦ β π΅ {β¨β¨π₯, π¦β©, πΆβ©} | ||
Theorem | cnvf1olem 6238 | Lemma for cnvf1o 6239. (Contributed by Mario Carneiro, 27-Apr-2014.) |
β’ ((Rel π΄ β§ (π΅ β π΄ β§ πΆ = βͺ β‘{π΅})) β (πΆ β β‘π΄ β§ π΅ = βͺ β‘{πΆ})) | ||
Theorem | cnvf1o 6239* | Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014.) |
β’ (Rel π΄ β (π₯ β π΄ β¦ βͺ β‘{π₯}):π΄β1-1-ontoββ‘π΄) | ||
Theorem | f2ndf 6240 | The 2nd (second component of an ordered pair) function restricted to a function πΉ is a function from πΉ into the codomain of πΉ. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβΆπ΅) | ||
Theorem | fo2ndf 6241 | The 2nd (second component of an ordered pair) function restricted to a function πΉ is a function from πΉ onto the range of πΉ. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβontoβran πΉ) | ||
Theorem | f1o2ndf1 6242 | The 2nd (second component of an ordered pair) function restricted to a one-to-one function πΉ is a one-to-one function from πΉ onto the range of πΉ. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
β’ (πΉ:π΄β1-1βπ΅ β (2nd βΎ πΉ):πΉβ1-1-ontoβran πΉ) | ||
Theorem | algrflem 6243 | Lemma for algrf and related theorems. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ π΅ β V & β’ πΆ β V β β’ (π΅(πΉ β 1st )πΆ) = (πΉβπ΅) | ||
Theorem | algrflemg 6244 | Lemma for algrf 12058 and related theorems. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Jim Kingdon, 22-Jul-2021.) |
β’ ((π΅ β π β§ πΆ β π) β (π΅(πΉ β 1st )πΆ) = (πΉβπ΅)) | ||
Theorem | xporderlem 6245* | Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅)) β§ ((1st βπ₯)π (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯)π(2nd βπ¦))))} β β’ (β¨π, πβ©πβ¨π, πβ© β (((π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π΅)) β§ (ππ π β¨ (π = π β§ πππ)))) | ||
Theorem | poxp 6246* | A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅)) β§ ((1st βπ₯)π (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯)π(2nd βπ¦))))} β β’ ((π Po π΄ β§ π Po π΅) β π Po (π΄ Γ π΅)) | ||
Theorem | spc2ed 6247* | Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
β’ β²π₯π & β’ β²π¦π & β’ ((π β§ (π₯ = π΄ β§ π¦ = π΅)) β (π β π)) β β’ ((π β§ (π΄ β π β§ π΅ β π)) β (π β βπ₯βπ¦π)) | ||
Theorem | cnvoprab 6248* | The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017.) |
β’ β²π₯π & β’ β²π¦π & β’ (π = β¨π₯, π¦β© β (π β π)) & β’ (π β π β (V Γ V)) β β’ β‘{β¨β¨π₯, π¦β©, π§β© β£ π} = {β¨π§, πβ© β£ π} | ||
Theorem | f1od2 6249* | Describe an implicit one-to-one onto function of two variables. (Contributed by Thierry Arnoux, 17-Aug-2017.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΅)) β πΆ β π) & β’ ((π β§ π§ β π·) β (πΌ β π β§ π½ β π)) & β’ (π β (((π₯ β π΄ β§ π¦ β π΅) β§ π§ = πΆ) β (π§ β π· β§ (π₯ = πΌ β§ π¦ = π½)))) β β’ (π β πΉ:(π΄ Γ π΅)β1-1-ontoβπ·) | ||
Theorem | disjxp1 6250* | The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β Disj π₯ β π΄ π΅) β β’ (π β Disj π₯ β π΄ (π΅ Γ πΆ)) | ||
Theorem | disjsnxp 6251* | The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ Disj π β π΄ ({π} Γ π΅) | ||
The following theorems are about maps-to operations (see df-mpo 5893) where the domain of the second argument depends on the domain of the first argument, especially when the first argument is a pair and the base set of the second argument is the first component of the first argument, in short "x-maps-to operations". For labels, the abbreviations "mpox" are used (since "x" usually denotes the first argument). This is in line with the currently used conventions for such cases (see cbvmpox 5966, ovmpox 6016 and fmpox 6214). If the first argument is an ordered pair, as in the following, the abbreviation is extended to "mpoxop", and the maps-to operations are called "x-op maps-to operations" for short. | ||
Theorem | opeliunxp2f 6252* | Membership in a union of Cartesian products, using bound-variable hypothesis for πΈ instead of distinct variable conditions as in opeliunxp2 4779. (Contributed by AV, 25-Oct-2020.) |
β’ β²π₯πΈ & β’ (π₯ = πΆ β π΅ = πΈ) β β’ (β¨πΆ, π·β© β βͺ π₯ β π΄ ({π₯} Γ π΅) β (πΆ β π΄ β§ π· β πΈ)) | ||
Theorem | mpoxopn0yelv 6253* | If there is an element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
β’ πΉ = (π₯ β V, π¦ β (1st βπ₯) β¦ πΆ) β β’ ((π β π β§ π β π) β (π β (β¨π, πβ©πΉπΎ) β πΎ β π)) | ||
Theorem | mpoxopoveq 6254* | Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
β’ πΉ = (π₯ β V, π¦ β (1st βπ₯) β¦ {π β (1st βπ₯) β£ π}) β β’ (((π β π β§ π β π) β§ πΎ β π) β (β¨π, πβ©πΉπΎ) = {π β π β£ [β¨π, πβ© / π₯][πΎ / π¦]π}) | ||
Theorem | mpoxopovel 6255* | Element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens and Mario Carneiro, 10-Oct-2017.) |
β’ πΉ = (π₯ β V, π¦ β (1st βπ₯) β¦ {π β (1st βπ₯) β£ π}) β β’ ((π β π β§ π β π) β (π β (β¨π, πβ©πΉπΎ) β (πΎ β π β§ π β π β§ [β¨π, πβ© / π₯][πΎ / π¦][π / π]π))) | ||
Theorem | rbropapd 6256* | Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
β’ (π β π = {β¨π, πβ© β£ (πππ β§ π)}) & β’ ((π = πΉ β§ π = π) β (π β π)) β β’ (π β ((πΉ β π β§ π β π) β (πΉππ β (πΉππ β§ π)))) | ||
Theorem | rbropap 6257* | Properties of a pair in a restricted binary relation π expressed as an ordered-pair class abstraction: π is the binary relation π restricted by the condition π. (Contributed by AV, 31-Jan-2021.) |
β’ (π β π = {β¨π, πβ© β£ (πππ β§ π)}) & β’ ((π = πΉ β§ π = π) β (π β π)) β β’ ((π β§ πΉ β π β§ π β π) β (πΉππ β (πΉππ β§ π))) | ||
Syntax | ctpos 6258 | The transposition of a function. |
class tpos πΉ | ||
Definition | df-tpos 6259* | Define the transposition of a function, which is a function πΊ = tpos πΉ satisfying πΊ(π₯, π¦) = πΉ(π¦, π₯). (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ tpos πΉ = (πΉ β (π₯ β (β‘dom πΉ βͺ {β }) β¦ βͺ β‘{π₯})) | ||
Theorem | tposss 6260 | Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (πΉ β πΊ β tpos πΉ β tpos πΊ) | ||
Theorem | tposeq 6261 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (πΉ = πΊ β tpos πΉ = tpos πΊ) | ||
Theorem | tposeqd 6262 | Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.) |
β’ (π β πΉ = πΊ) β β’ (π β tpos πΉ = tpos πΊ) | ||
Theorem | tposssxp 6263 | The transposition is a subset of a cross product. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ tpos πΉ β ((β‘dom πΉ βͺ {β }) Γ ran πΉ) | ||
Theorem | reltpos 6264 | The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ Rel tpos πΉ | ||
Theorem | brtpos2 6265 | Value of the transposition at a pair β¨π΄, π΅β©. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (π΅ β π β (π΄tpos πΉπ΅ β (π΄ β (β‘dom πΉ βͺ {β }) β§ βͺ β‘{π΄}πΉπ΅))) | ||
Theorem | brtpos0 6266 | The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (π΄ β π β (β tpos πΉπ΄ β β πΉπ΄)) | ||
Theorem | reldmtpos 6267 | Necessary and sufficient condition for dom tpos πΉ to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (Rel dom tpos πΉ β Β¬ β β dom πΉ) | ||
Theorem | brtposg 6268 | The transposition swaps arguments of a three-parameter relation. (Contributed by Jim Kingdon, 31-Jan-2019.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (β¨π΄, π΅β©tpos πΉπΆ β β¨π΅, π΄β©πΉπΆ)) | ||
Theorem | ottposg 6269 | The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (β¨π΄, π΅, πΆβ© β tpos πΉ β β¨π΅, π΄, πΆβ© β πΉ)) | ||
Theorem | dmtpos 6270 | The domain of tpos πΉ when dom πΉ is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (Rel dom πΉ β dom tpos πΉ = β‘dom πΉ) | ||
Theorem | rntpos 6271 | The range of tpos πΉ when dom πΉ is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (Rel dom πΉ β ran tpos πΉ = ran πΉ) | ||
Theorem | tposexg 6272 | The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (πΉ β π β tpos πΉ β V) | ||
Theorem | ovtposg 6273 | The transposition swaps the arguments in a two-argument function. When πΉ is a matrix, which is to say a function from ( 1 ... m ) Γ ( 1 ... n ) to the reals or some ring, tpos πΉ is the transposition of πΉ, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄tpos πΉπ΅) = (π΅πΉπ΄)) | ||
Theorem | tposfun 6274 | The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (Fun πΉ β Fun tpos πΉ) | ||
Theorem | dftpos2 6275* | Alternate definition of tpos when πΉ has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (Rel dom πΉ β tpos πΉ = (πΉ β (π₯ β β‘dom πΉ β¦ βͺ β‘{π₯}))) | ||
Theorem | dftpos3 6276* | Alternate definition of tpos when πΉ has relational domain. Compare df-cnv 4646. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ (Rel dom πΉ β tpos πΉ = {β¨β¨π₯, π¦β©, π§β© β£ β¨π¦, π₯β©πΉπ§}) | ||
Theorem | dftpos4 6277* | Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ tpos πΉ = (πΉ β (π₯ β ((V Γ V) βͺ {β }) β¦ βͺ β‘{π₯})) | ||
Theorem | tpostpos 6278 | Value of the double transposition for a general class πΉ. (Contributed by Mario Carneiro, 16-Sep-2015.) |
β’ tpos tpos πΉ = (πΉ β© (((V Γ V) βͺ {β }) Γ V)) | ||
Theorem | tpostpos2 6279 | Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.) |
β’ ((Rel πΉ β§ Rel dom πΉ) β tpos tpos πΉ = πΉ) | ||
Theorem | tposfn2 6280 | The domain of a transposition. (Contributed by NM, 10-Sep-2015.) |
β’ (Rel π΄ β (πΉ Fn π΄ β tpos πΉ Fn β‘π΄)) | ||
Theorem | tposfo2 6281 | Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.) |
β’ (Rel π΄ β (πΉ:π΄βontoβπ΅ β tpos πΉ:β‘π΄βontoβπ΅)) | ||
Theorem | tposf2 6282 | The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.) |
β’ (Rel π΄ β (πΉ:π΄βΆπ΅ β tpos πΉ:β‘π΄βΆπ΅)) | ||
Theorem | tposf12 6283 | Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.) |
β’ (Rel π΄ β (πΉ:π΄β1-1βπ΅ β tpos πΉ:β‘π΄β1-1βπ΅)) | ||
Theorem | tposf1o2 6284 | Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.) |
β’ (Rel π΄ β (πΉ:π΄β1-1-ontoβπ΅ β tpos πΉ:β‘π΄β1-1-ontoβπ΅)) | ||
Theorem | tposfo 6285 | The domain and codomain/range of a transposition. (Contributed by NM, 10-Sep-2015.) |
β’ (πΉ:(π΄ Γ π΅)βontoβπΆ β tpos πΉ:(π΅ Γ π΄)βontoβπΆ) | ||
Theorem | tposf 6286 | The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.) |
β’ (πΉ:(π΄ Γ π΅)βΆπΆ β tpos πΉ:(π΅ Γ π΄)βΆπΆ) | ||
Theorem | tposfn 6287 | Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (πΉ Fn (π΄ Γ π΅) β tpos πΉ Fn (π΅ Γ π΄)) | ||
Theorem | tpos0 6288 | Transposition of the empty set. (Contributed by NM, 10-Sep-2015.) |
β’ tpos β = β | ||
Theorem | tposco 6289 | Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ tpos (πΉ β πΊ) = (πΉ β tpos πΊ) | ||
Theorem | tpossym 6290* | Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (πΉ Fn (π΄ Γ π΄) β (tpos πΉ = πΉ β βπ₯ β π΄ βπ¦ β π΄ (π₯πΉπ¦) = (π¦πΉπ₯))) | ||
Theorem | tposeqi 6291 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ πΉ = πΊ β β’ tpos πΉ = tpos πΊ | ||
Theorem | tposex 6292 | A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ πΉ β V β β’ tpos πΉ β V | ||
Theorem | nftpos 6293 | Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ β²π₯πΉ β β’ β²π₯tpos πΉ | ||
Theorem | tposoprab 6294* | Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ πΉ = {β¨β¨π₯, π¦β©, π§β© β£ π} β β’ tpos πΉ = {β¨β¨π¦, π₯β©, π§β© β£ π} | ||
Theorem | tposmpo 6295* | Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) β β’ tpos πΉ = (π¦ β π΅, π₯ β π΄ β¦ πΆ) | ||
Theorem | pwuninel2 6296 | The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (βͺ π΄ β π β Β¬ π« βͺ π΄ β π΄) | ||
Theorem | 2pwuninelg 6297 | The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.) |
β’ (π΄ β π β Β¬ π« π« βͺ π΄ β π΄) | ||
Theorem | iunon 6298* | The indexed union of a set of ordinal numbers π΅(π₯) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 5-Dec-2016.) |
β’ ((π΄ β π β§ βπ₯ β π΄ π΅ β On) β βͺ π₯ β π΄ π΅ β On) | ||
Syntax | wsmo 6299 | Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals. |
wff Smo π΄ | ||
Definition | df-smo 6300* | Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 15-Nov-2011.) |
β’ (Smo π΄ β (π΄:dom π΄βΆOn β§ Ord dom π΄ β§ βπ₯ β dom π΄βπ¦ β dom π΄(π₯ β π¦ β (π΄βπ₯) β (π΄βπ¦)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |