P. 59 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5801-5900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ot3rdgg 5801	Extract the third member of an ordered triple. (See ot1stg 5799 comment.) (Contributed by NM, 3-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( 2nd ` <. A , B , C >. ) = C )
Theorem	1stval2 5802	Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
|- ( A e. ( _V X. _V ) -> ( 1st ` A ) = |^| |^| A )
Theorem	2ndval2 5803	Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
|- ( A e. ( _V X. _V ) -> ( 2nd ` A ) = |^| |^| |^| `' { A } )
Theorem	fo1st 5804	The 1st function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- 1st : _V -onto-> _V
Theorem	fo2nd 5805	The 2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- 2nd : _V -onto-> _V
Theorem	f1stres 5806	Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( 1st |` ( A X. B ) ) : ( A X. B ) --> A
Theorem	f2ndres 5807	Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( 2nd |` ( A X. B ) ) : ( A X. B ) --> B
Theorem	fo1stresm 5808*	Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|- ( E. y y e. B -> ( 1st |` ( A X. B ) ) : ( A X. B ) -onto-> A )
Theorem	fo2ndresm 5809*	Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|- ( E. x x e. A -> ( 2nd |` ( A X. B ) ) : ( A X. B ) -onto-> B )
Theorem	1stcof 5810	Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.)
|- ( F : A --> ( B X. C ) -> ( 1st o. F ) : A --> B )
Theorem	2ndcof 5811	Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.)
|- ( F : A --> ( B X. C ) -> ( 2nd o. F ) : A --> C )
Theorem	xp1st 5812	Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. ( B X. C ) -> ( 1st ` A ) e. B )
Theorem	xp2nd 5813	Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. ( B X. C ) -> ( 2nd ` A ) e. C )
Theorem	1stexg 5814	Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.)
|- ( A e. V -> ( 1st ` A ) e. _V )
Theorem	2ndexg 5815	Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.)
|- ( A e. V -> ( 2nd ` A ) e. _V )
Theorem	elxp6 5816	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp4 4828. (Contributed by NM, 9-Oct-2004.)
|- ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
Theorem	elxp7 5817	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp4 4828. (Contributed by NM, 19-Aug-2006.)
|- ( A e. ( B X. C ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
Theorem	eqopi 5818	Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.)
|- ( ( A e. ( V X. W ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) -> A = <. B , C >. )
Theorem	xp2 5819*	Representation of cross product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.)
|- ( A X. B ) = { x e. ( _V X. _V ) | ( ( 1st ` x ) e. A /\ ( 2nd ` x ) e. B ) }
Theorem	unielxp 5820	The membership relation for a cross product is inherited by union. (Contributed by NM, 16-Sep-2006.)
|- ( A e. ( B X. C ) -> U. A e. U. ( B X. C ) )
Theorem	1st2nd2 5821	Reconstruction of a member of a cross product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013.)
|- ( A e. ( B X. C ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
Theorem	xpopth 5822	An ordered pair theorem for members of cross products. (Contributed by NM, 20-Jun-2007.)
|- ( ( A e. ( C X. D ) /\ B e. ( R X. S ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> A = B ) )
Theorem	eqop 5823	Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
|- ( A e. ( V X. W ) -> ( A = <. B , C >. <-> ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) )
Theorem	eqop2 5824	Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.)
|- B e. _V   &    |- C e. _V   =>    |- ( A = <. B , C >. <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) )
Theorem	op1steq 5825*	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.)
|- ( A e. ( V X. W ) -> ( ( 1st ` A ) = B <-> E. x A = <. B , x >. ) )
Theorem	2nd1st 5826	Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.)
|- ( A e. ( B X. C ) -> U. `' { A } = <. ( 2nd ` A ) , ( 1st ` A ) >. )
Theorem	1st2nd 5827	Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006.)
|- ( ( Rel B /\ A e. B ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
Theorem	1stdm 5828	The first ordered pair component of a member of a relation belongs to the domain of the relation. (Contributed by NM, 17-Sep-2006.)
|- ( ( Rel R /\ A e. R ) -> ( 1st ` A ) e. dom R )
Theorem	2ndrn 5829	The second ordered pair component of a member of a relation belongs to the range of the relation. (Contributed by NM, 17-Sep-2006.)
|- ( ( Rel R /\ A e. R ) -> ( 2nd ` A ) e. ran R )
Theorem	1st2ndbr 5830	Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.)
|- ( ( Rel B /\ A e. B ) -> ( 1st ` A ) B ( 2nd ` A ) )
Theorem	releldm2 5831*	Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013.)
|- ( Rel A -> ( B e. dom A <-> E. x e. A ( 1st ` x ) = B ) )
Theorem	reldm 5832*	An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013.)
|- ( Rel A -> dom A = ran ( x e. A |-> ( 1st ` x ) ) )
Theorem	sbcopeq1a 5833	Equality theorem for substitution of a class for an ordered pair (analog of sbceq1a 2824 that avoids the existential quantifiers of copsexg 3999). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( A = <. x , y >. -> ( [. ( 1st ` A ) / x ]. [. ( 2nd ` A ) / y ]. ph <-> ph ) )
Theorem	csbopeq1a 5834	Equality theorem for substitution of a class A for an ordered pair <. x , y >. in B (analog of csbeq1a 2916). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( A = <. x , y >. -> [_ ( 1st ` A ) / x ]_ [_ ( 2nd ` A ) / y ]_ B = B )
Theorem	dfopab2 5835*	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.)
|- { <. x , y >. | ph } = { z e. ( _V X. _V ) | [. ( 1st ` z ) / x ]. [. ( 2nd ` z ) / y ]. ph }
Theorem	dfoprab3s 5836*	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.)
|- { <. <. x , y >. , z >. | ph } = { <. w , z >. | ( w e. ( _V X. _V ) /\ [. ( 1st ` w ) / x ]. [. ( 2nd ` w ) / y ]. ph ) }
Theorem	dfoprab3 5837*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.)
|- ( w = <. x , y >. -> ( ph <-> ps ) )   =>    |- { <. w , z >. | ( w e. ( _V X. _V ) /\ ph ) } = { <. <. x , y >. , z >. | ps }
Theorem	dfoprab4 5838*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- ( w = <. x , y >. -> ( ph <-> ps ) )   =>    |- { <. w , z >. | ( w e. ( A X. B ) /\ ph ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) }
Theorem	dfoprab4f 5839*	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.)
|- F/ x ph   &    |- F/ y ph   &    |- ( w = <. x , y >. -> ( ph <-> ps ) )   =>    |- { <. w , z >. | ( w e. ( A X. B ) /\ ph ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) }
Theorem	dfxp3 5840*	Define the cross product of three classes. Compare df-xp 4369. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.)
|- ( ( A X. B ) X. C ) = { <. <. x , y >. , z >. | ( x e. A /\ y e. B /\ z e. C ) }
Theorem	elopabi 5841*	A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.)
|- ( x = ( 1st ` A ) -> ( ph <-> ps ) )   &    |- ( y = ( 2nd ` A ) -> ( ps <-> ch ) )   =>    |- ( A e. { <. x , y >. | ph } -> ch )
Theorem	eloprabi 5842*	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.)
|- ( x = ( 1st ` ( 1st ` A ) ) -> ( ph <-> ps ) )   &    |- ( y = ( 2nd ` ( 1st ` A ) ) -> ( ps <-> ch ) )   &    |- ( z = ( 2nd ` A ) -> ( ch <-> th ) )   =>    |- ( A e. { <. <. x , y >. , z >. | ph } -> th )
Theorem	mpt2mptsx 5843*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( x e. A , y e. B |-> C ) = ( z e. U_ x e. A ( { x } X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )
Theorem	mpt2mpts 5844*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.)
|- ( x e. A , y e. B |-> C ) = ( z e. ( A X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )
Theorem	dmmpt2ssx 5845*	The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- dom F C_ U_ x e. A ( { x } X. B )
Theorem	fmpt2x 5846*	Functionality, domain and codomain of a class given by the "maps to" notation, where B ( x ) is not constant but depends on x. (Contributed by NM, 29-Dec-2014.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( A. x e. A A. y e. B C e. D <-> F : U_ x e. A ( { x } X. B ) --> D )
Theorem	fmpt2 5847*	Functionality, domain and range of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( A. x e. A A. y e. B C e. D <-> F : ( A X. B ) --> D )
Theorem	fnmpt2 5848*	Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( A. x e. A A. y e. B C e. V -> F Fn ( A X. B ) )
Theorem	mpt2fvex 5849*	Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( A. x A. y C e. V /\ R e. W /\ S e. X ) -> ( R F S ) e. _V )
Theorem	fnmpt2i 5850*	Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
|- F = ( x e. A , y e. B |-> C )   &    |- C e. _V   =>    |- F Fn ( A X. B )
Theorem	dmmpt2 5851*	Domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
|- F = ( x e. A , y e. B |-> C )   &    |- C e. _V   =>    |- dom F = ( A X. B )
Theorem	mpt2fvexi 5852*	Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- F = ( x e. A , y e. B |-> C )   &    |- C e. _V   &    |- R e. _V   &    |- S e. _V   =>    |- ( R F S ) e. _V
Theorem	mpt2exxg 5853*	Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( A e. R /\ A. x e. A B e. S ) -> F e. _V )
Theorem	mpt2exg 5854*	Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( A e. R /\ B e. S ) -> F e. _V )
Theorem	mpt2exga 5855*	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.)
|- ( ( A e. V /\ B e. W ) -> ( x e. A , y e. B |-> C ) e. _V )
Theorem	mpt2ex 5856*	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.)
|- A e. _V   &    |- B e. _V   =>    |- ( x e. A , y e. B |-> C ) e. _V
Theorem	fmpt2co 5857*	Composition of two functions. Variation of fmptco 5351 when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> R e. C )   &    |- ( ph -> F = ( x e. A , y e. B |-> R ) )   &    |- ( ph -> G = ( z e. C |-> S ) )   &    |- ( z = R -> S = T )   =>    |- ( ph -> ( G o. F ) = ( x e. A , y e. B |-> T ) )
Theorem	oprabco 5858*	Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 26-Sep-2015.)
|- ( ( x e. A /\ y e. B ) -> C e. D )   &    |- F = ( x e. A , y e. B |-> C )   &    |- G = ( x e. A , y e. B |-> ( H ` C ) )   =>    |- ( H Fn D -> G = ( H o. F ) )
Theorem	oprab2co 5859*	Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by David Abernethy, 23-Apr-2013.)
|- ( ( x e. A /\ y e. B ) -> C e. R )   &    |- ( ( x e. A /\ y e. B ) -> D e. S )   &    |- F = ( x e. A , y e. B |-> <. C , D >. )   &    |- G = ( x e. A , y e. B |-> ( C M D ) )   =>    |- ( M Fn ( R X. S ) -> G = ( M o. F ) )
Theorem	df1st2 5860*	An alternate possible definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- { <. <. x , y >. , z >. | z = x } = ( 1st |` ( _V X. _V ) )
Theorem	df2nd2 5861*	An alternate possible definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- { <. <. x , y >. , z >. | z = y } = ( 2nd |` ( _V X. _V ) )
Theorem	1stconst 5862	The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008.)
|- ( B e. V -> ( 1st |` ( A X. { B } ) ) : ( A X. { B } ) -1-1-onto-> A )
Theorem	2ndconst 5863	The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008.)
|- ( A e. V -> ( 2nd |` ( { A } X. B ) ) : ( { A } X. B ) -1-1-onto-> B )
Theorem	dfmpt2 5864*	Alternate definition for the "maps to" notation df-mpt2 5537 (although it requires that C be a set). (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- C e. _V   =>    |- ( x e. A , y e. B |-> C ) = U_ x e. A U_ y e. B { <. <. x , y >. , C >. }
Theorem	cnvf1olem 5865	Lemma for cnvf1o 5866. (Contributed by Mario Carneiro, 27-Apr-2014.)
|- ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> ( C e. `' A /\ B = U. `' { C } ) )
Theorem	cnvf1o 5866*	Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014.)
|- ( Rel A -> ( x e. A |-> U. `' { x } ) : A -1-1-onto-> `' A )
Theorem	f2ndf 5867	The 2nd (second member of an ordered pair) function restricted to a function F is a function of F into the codomain of F. (Contributed by Alexander van der Vekens, 4-Feb-2018.)
|- ( F : A --> B -> ( 2nd |` F ) : F --> B )
Theorem	fo2ndf 5868	The 2nd (second member of an ordered pair) function restricted to a function F is a function of F onto the range of F. (Contributed by Alexander van der Vekens, 4-Feb-2018.)
|- ( F : A --> B -> ( 2nd |` F ) : F -onto-> ran F )
Theorem	f1o2ndf1 5869	The 2nd (second member of an ordered pair) function restricted to a one-to-one function F is a one-to-one function of F onto the range of F. (Contributed by Alexander van der Vekens, 4-Feb-2018.)
|- ( F : A -1-1-> B -> ( 2nd |` F ) : F -1-1-onto-> ran F )
Theorem	algrflem 5870	Lemma for algrf and related theorems. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- B e. _V   &    |- C e. _V   =>    |- ( B ( F o. 1st ) C ) = ( F ` B )
Theorem	algrflemg 5871	Lemma for algrf and related theorems. (Contributed by Jim Kingdon, 22-Jul-2021.)
|- ( ( B e. V /\ C e. W ) -> ( B ( F o. 1st ) C ) = ( F ` B ) )
Theorem	xporderlem 5872*	Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.)
|- T = { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) }   =>    |- ( <. a , b >. T <. c , d >. <-> ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) )
Theorem	poxp 5873*	A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)
|- T = { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) }   =>    |- ( ( R Po A /\ S Po B ) -> T Po ( A X. B ) )
Theorem	spc2ed 5874*	Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.)
|- F/ x ch   &    |- F/ y ch   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )   =>    |- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( ch -> E. x E. y ps ) )
Theorem	cnvoprab 5875*	The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017.)
|- F/ x ps   &    |- F/ y ps   &    |- ( a = <. x , y >. -> ( ps <-> ph ) )   &    |- ( ps -> a e. ( _V X. _V ) )   =>    |- `' { <. <. x , y >. , z >. | ph } = { <. z , a >. | ps }
Theorem	f1od2 5876*	Describe an implicit one-to-one onto function of two variables. (Contributed by Thierry Arnoux, 17-Aug-2017.)
|- F = ( x e. A , y e. B |-> C )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. W )   &    |- ( ( ph /\ z e. D ) -> ( I e. X /\ J e. Y ) )   &    |- ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( z e. D /\ ( x = I /\ y = J ) ) ) )   =>    |- ( ph -> F : ( A X. B ) -1-1-onto-> D )
2.6.15  Special "Maps to" operations The following theorems are about maps-to operations (see df-mpt2 5537) where 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 "mpt2x" are used (since "x" usually denotes the first argument). This is in line with the currently used conventions for such cases (see cbvmpt2x 5602, ovmpt2x 5649 and fmpt2x 5846). However, there is a proposal by Norman Megill to use the abbreviation "mpo" or "mpto" instead of "mpt2" (see beginning of set.mm). If this proposal will be realized, the labels in the following should also be adapted. If the first argument is an ordered pair, as in the following, the abbreviation is extended to "mpt2xop", and the maps-to operations are called "x-op maps-to operations" for short.
Theorem	mpt2xopn0yelv 5877*	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.)
|- F = ( x e. _V , y e. ( 1st ` x ) |-> C )   =>    |- ( ( V e. X /\ W e. Y ) -> ( N e. ( <. V , W >. F K ) -> K e. V ) )
Theorem	mpt2xopoveq 5878*	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.)
|- F = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | ph } )   =>    |- ( ( ( V e. X /\ W e. Y ) /\ K e. V ) -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
Theorem	mpt2xopovel 5879*	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.)
|- F = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | ph } )   =>    |- ( ( V e. X /\ W e. Y ) -> ( N e. ( <. V , W >. F K ) <-> ( K e. V /\ N e. V /\ [. <. V , W >. / x ]. [. K / y ]. [. N / n ]. ph ) ) )
Theorem	sprmpt2 5880*	The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
|- M = ( v e. _V , e e. _V |-> { <. f , p >. | ( f ( v W e ) p /\ ch ) } )   &    |- ( ( v = V /\ e = E ) -> ( ch <-> ps ) )   &    |- ( ( V e. _V /\ E e. _V ) -> ( f ( V W E ) p -> th ) )   &    |- ( ( V e. _V /\ E e. _V ) -> { <. f , p >. | th } e. _V )   =>    |- ( ( V e. _V /\ E e. _V ) -> ( V M E ) = { <. f , p >. | ( f ( V W E ) p /\ ps ) } )
Theorem	isprmpt2 5881*	Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
|- ( ph -> M = { <. f , p >. | ( f W p /\ ps ) } )   &    |- ( ( f = F /\ p = P ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch ) ) ) )
2.6.16  Function transposition
Syntax	ctpos 5882	The transposition of a function.
class tpos F
Definition	df-tpos 5883*	Define the transposition of a function, which is a function G = tpos F satisfying G ( x , y ) = F ( y , x ). (Contributed by Mario Carneiro, 10-Sep-2015.)
|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
Theorem	tposss 5884	Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( F C_ G -> tpos F C_ tpos G )
Theorem	tposeq 5885	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( F = G -> tpos F = tpos G )
Theorem	tposeqd 5886	Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> F = G )   =>    |- ( ph -> tpos F = tpos G )
Theorem	tposssxp 5887	The transposition is a subset of a cross product. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F )
Theorem	reltpos 5888	The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- Rel tpos F
Theorem	brtpos2 5889	Value of the transposition at a pair <. A , B >.. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( B e. V -> ( Atpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) )
Theorem	brtpos0 5890	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.)
|- ( A e. V -> ( (/)tpos F A <-> (/) F A ) )
Theorem	reldmtpos 5891	Necessary and sufficient condition for dom tpos F to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom tpos F <-> -. (/) e. dom F )
Theorem	brtposg 5892	The transposition swaps arguments of a three-parameter relation. (Contributed by Jim Kingdon, 31-Jan-2019.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. A , B >.tpos F C <-> <. B , A >. F C ) )
Theorem	ottposg 5893	The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. A , B , C >. e. tpos F <-> <. B , A , C >. e. F ) )
Theorem	dmtpos 5894	The domain of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> dom tpos F = `' dom F )
Theorem	rntpos 5895	The range of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> ran tpos F = ran F )
Theorem	tposexg 5896	The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( F e. V -> tpos F e. _V )
Theorem	ovtposg 5897	The transposition swaps the arguments in a two-argument function. When F is a matrix, which is to say a function from ( 1 ... m ) X. ( 1 ... n ) to the reals or some ring, tpos F is the transposition of F, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( ( A e. V /\ B e. W ) -> ( Atpos F B ) = ( B F A ) )
Theorem	tposfun 5898	The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Fun F -> Fun tpos F )
Theorem	dftpos2 5899*	Alternate definition of tpos when F has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> tpos F = ( F o. ( x e. `' dom F |-> U. `' { x } ) ) )
Theorem	dftpos3 5900*	Alternate definition of tpos when F has relational domain. Compare df-cnv 4371. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> tpos F = { <. <. x , y >. , z >. | <. y , x >. F z } )