P. 70 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6901-7000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	df1st2 6901*	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 6902*	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 6903	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 6904	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 6905*	Alternate definition for the "maps to" notation df-mpt2 6313 (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	mpt2sn 6906*	An operation (in maps-to notation) on two singletons. (Contributed by AV, 4-Aug-2019.)
|- F = ( x e. { A } , y e. { B } |-> C )   &    |- ( x = A -> C = D )   &    |- ( y = B -> D = E )   =>    |- ( ( A e. V /\ B e. W /\ E e. U ) -> F = { <. <. A , B >. , E >. } )
Theorem	curry1 6907*	Composition with `' ( 2nd |` ( { C } X. _V ) ) turns any binary operation F with a constant first operand into a function G of the second operand only. This transformation is called "currying." (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Dec-2014.)
|- G = ( F o. `' ( 2nd |` ( { C } X. _V ) ) )   =>    |- ( ( F Fn ( A X. B ) /\ C e. A ) -> G = ( x e. B |-> ( C F x ) ) )
Theorem	curry1val 6908	The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- G = ( F o. `' ( 2nd |` ( { C } X. _V ) ) )   =>    |- ( ( F Fn ( A X. B ) /\ C e. A ) -> ( G ` D ) = ( C F D ) )
Theorem	curry1f 6909	Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008.)
|- G = ( F o. `' ( 2nd |` ( { C } X. _V ) ) )   =>    |- ( ( F : ( A X. B ) --> D /\ C e. A ) -> G : B --> D )
Theorem	curry2 6910*	Composition with `' ( 1st |` ( _V X. { C } ) ) turns any binary operation F with a constant second operand into a function G of the first operand only. This transformation is called "currying." (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008.)
|- G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )   =>    |- ( ( F Fn ( A X. B ) /\ C e. B ) -> G = ( x e. A |-> ( x F C ) ) )
Theorem	curry2f 6911	Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.)
|- G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )   =>    |- ( ( F : ( A X. B ) --> D /\ C e. B ) -> G : A --> D )
Theorem	curry2val 6912	The value of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.)
|- G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )   =>    |- ( ( F Fn ( A X. B ) /\ C e. B ) -> ( G ` D ) = ( D F C ) )
Theorem	cnvf1olem 6913	Lemma for cnvf1o 6914. (Contributed by Mario Carneiro, 27-Apr-2014.)
|- ( ( Rel A /\ ( B e. A /\ C = U. `' { B } ) ) -> ( C e. `' A /\ B = U. `' { C } ) )
Theorem	cnvf1o 6914*	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	fparlem1 6915	Lemma for fpar 6919. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( `' ( 1st |` ( _V X. _V ) ) " { x } ) = ( { x } X. _V )
Theorem	fparlem2 6916	Lemma for fpar 6919. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( `' ( 2nd |` ( _V X. _V ) ) " { y } ) = ( _V X. { y } )
Theorem	fparlem3 6917*	Lemma for fpar 6919. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( F Fn A -> ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) = U_ x e. A ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) )
Theorem	fparlem4 6918*	Lemma for fpar 6919. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( G Fn B -> ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) = U_ y e. B ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) )
Theorem	fpar 6919*	Merge two functions in parallel. Use as the second argument of a composition with a (2-place) operation to build compound operations such as z = ( ( sqr ` x ) + ( abs ` y ) ). (Contributed by NM, 17-Sep-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
|- H = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) )   =>    |- ( ( F Fn A /\ G Fn B ) -> H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) )
Theorem	fsplit 6920	A function that can be used to feed a common value to both operands of an operation. Use as the second argument of a composition with the function of fpar 6919 in order to build compound functions such as y = ( ( sqr ` x ) + ( abs ` x ) ). (Contributed by NM, 17-Sep-2007.)
|- `' ( 1st |` _I ) = ( x e. _V |-> <. x , x >. )
Theorem	f2ndf 6921	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 6922	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 6923	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 6924	Lemma for algrf 14611 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	frxp 6925*	A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) (Proof shortened by Wolf Lammen, 4-Oct-2014.)
|- 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 Fr A /\ S Fr B ) -> T Fr ( A X. B ) )
Theorem	xporderlem 6926*	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 6927*	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	soxp 6928*	A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-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 Or A /\ S Or B ) -> T Or ( A X. B ) )
Theorem	wexp 6929*	A lexicographical ordering of two well-ordered classes. (Contributed by Scott Fenton, 17-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 We A /\ S We B ) -> T We ( A X. B ) )
Theorem	fnwelem 6930*	Lemma for fnwe 6931. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)
|- T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) }   &    |- ( ph -> F : A --> B )   &    |- ( ph -> R We B )   &    |- ( ph -> S We A )   &    |- ( ph -> ( F " w ) e. _V )   &    |- Q = { <. u , v >. | ( ( u e. ( B X. A ) /\ v e. ( B X. A ) ) /\ ( ( 1st ` u ) R ( 1st ` v ) \/ ( ( 1st ` u ) = ( 1st ` v ) /\ ( 2nd ` u ) S ( 2nd ` v ) ) ) ) }   &    |- G = ( z e. A |-> <. ( F ` z ) , z >. )   =>    |- ( ph -> T We A )
Theorem	fnwe 6931*	A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)
|- T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) }   &    |- ( ph -> F : A --> B )   &    |- ( ph -> R We B )   &    |- ( ph -> S We A )   &    |- ( ph -> ( F " w ) e. _V )   =>    |- ( ph -> T We A )
Theorem	fnse 6932*	Condition for the well-order in fnwe 6931 to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015.)
|- T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) }   &    |- ( ph -> F : A --> B )   &    |- ( ph -> R Se B )   &    |- ( ph -> ( `' F " w ) e. _V )   =>    |- ( ph -> T Se A )
2.4.8  The support of functions In this section, the support of functions is defined and corresponding theorems are provided. Since basic properties (see suppval 6935) are based on the Axiom of Union (usage of dmexg 6743), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression ( `' R " ( _V \ { Z } ) ) (see suppimacnv 6944). The theorems which are based on this representation and which are provided in previous sections could be moved into this section to have all related theorems in one section, although they do not depend on the Axiom of Union. This was possible because they are not used before. The current theorems differ from the original ones by requiring that the classes representing the "function" (or its "domain") and the "zero element" are sets. Actually, this does not cause any problem (until now).
Syntax	csupp 6933	Extend class definition to include the support of functions.
class supp
Definition	df-supp 6934*	Define the support of a function against a "zero" value. According to Wikipedia ("Support (mathematics)", 31-Mar-2019, https://en.wikipedia.org/wiki/Support_(mathematics)) "In mathematics, the support of a real-valued function f is the subset of the domain containing those elements which are not mapped to zero." and "The notion of support also extends in a natural way to functions taking values in more general sets than R [the real numbers] and to other objects.". The following definition allows for such extensions, being applicable for any sets (which usually are functions) and any element (even not necessarily from the range of the function) regarded as "zero". (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.)
|- supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
Theorem	suppval 6935*	The value of the operation constructing the support of a function. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.)
|- ( ( X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X " { i } ) =/= { Z } } )
Theorem	supp0prc 6936	The support of a class is empty if either the class or the "zero" is a proper class. . (Contributed by AV, 28-May-2019.)
|- ( -. ( X e. _V /\ Z e. _V ) -> ( X supp Z ) = (/) )
Theorem	suppvalbr 6937*	The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019.)
|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } )
Theorem	supp0 6938	The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019.)
|- ( Z e. W -> ( (/) supp Z ) = (/) )
Theorem	suppval1 6939*	The value of the operation constructing the support of a function. (Contributed by AV, 6-Apr-2019.)
|- ( ( Fun X /\ X e. V /\ Z e. W ) -> ( X supp Z ) = { i e. dom X | ( X ` i ) =/= Z } )
Theorem	suppvalfn 6940*	The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by AV, 22-Apr-2019.)
|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )
Theorem	elsuppfn 6941	An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019.)
|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( S e. ( F supp Z ) <-> ( S e. X /\ ( F ` S ) =/= Z ) ) )
Theorem	cnvimadfsn 6942*	The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019.)
|- ( `' R " ( _V \ { Z } ) ) = { x | E. y ( x R y /\ y =/= Z ) }
Theorem	suppimacnvss 6943	The support of functions "defined" by inverse images is a subset of the support defined by df-supp 6934. (Contributed by AV, 7-Apr-2019.)
|- ( ( R e. V /\ Z e. W ) -> ( `' R " ( _V \ { Z } ) ) C_ ( R supp Z ) )
Theorem	suppimacnv 6944	Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 7-Apr-2019.)
|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = ( `' R " ( _V \ { Z } ) ) )
Theorem	frnsuppeq 6945	Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.)
|- ( ( I e. V /\ Z e. W ) -> ( F : I --> S -> ( F supp Z ) = ( `' F " ( S \ { Z } ) ) ) )
Theorem	suppssdm 6946	The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.)
|- ( F supp Z ) C_ dom F
Theorem	suppsnop 6947	The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019.)
|- F = { <. X , Y >. }   =>    |- ( ( X e. V /\ Y e. W /\ Z e. U ) -> ( F supp Z ) = if ( Y = Z , (/) , { X } ) )
Theorem	snopsuppss 6948	The support of a singleton containing an ordered pair is a subset of the singleton containing the first element of the ordered pair, i.e. it is empty or the singleton itself. (Contributed by AV, 19-Jul-2019.)
|- ( { <. X , Y >. } supp Z ) C_ { X }
Theorem	fvn0elsupp 6949	If the function value for a given argument is not empty, the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 2-Jul-2019.) (Revised by AV, 4-Apr-2020.)
|- ( ( ( B e. V /\ X e. B ) /\ ( G Fn B /\ ( G ` X ) =/= (/) ) ) -> X e. ( G supp (/) ) )
Theorem	fvn0elsuppOLD 6950	Obsolete version of fvn0elsupp 6949 as of 4-Apr-2020. (Contributed by AV, 2-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( B e. V /\ X e. B ) /\ ( G : B --> A /\ ( G ` X ) =/= (/) ) ) -> X e. ( G supp (/) ) )
Theorem	fvn0elsuppb 6951	The function value for a given argument is not empty iff the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 4-Apr-2020.)
|- ( ( B e. V /\ X e. B /\ G Fn B ) -> ( ( G ` X ) =/= (/) <-> X e. ( G supp (/) ) ) )
Theorem	rexsupp 6952*	Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by AV, 27-May-2019.)
|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( E. x e. ( F supp Z ) ph <-> E. x e. X ( ( F ` x ) =/= Z /\ ph ) ) )
Theorem	ressuppss 6953	The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.)
|- ( ( F e. V /\ Z e. W ) -> ( ( F |` B ) supp Z ) C_ ( F supp Z ) )
Theorem	suppun 6954	The support of a class/function is a subset of the support of the union of this class/function with another class/function. (Contributed by AV, 4-Jun-2019.)
|- ( ph -> G e. V )   =>    |- ( ph -> ( F supp Z ) C_ ( ( F u. G ) supp Z ) )
Theorem	ressuppssdif 6955	The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.)
|- ( ( F e. V /\ Z e. W ) -> ( F supp Z ) C_ ( ( ( F |` B ) supp Z ) u. ( dom F \ B ) ) )
Theorem	mptsuppdifd 6956*	The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019.)
|- F = ( x e. A |-> B )   &    |- ( ph -> A e. V )   &    |- ( ph -> Z e. W )   =>    |- ( ph -> ( F supp Z ) = { x e. A | B e. ( _V \ { Z } ) } )
Theorem	mptsuppd 6957*	The support of a function in maps-to notation. (Contributed by AV, 10-Apr-2019.) (Revised by AV, 28-May-2019.)
|- F = ( x e. A |-> B )   &    |- ( ph -> A e. V )   &    |- ( ph -> Z e. W )   &    |- ( ( ph /\ x e. A ) -> B e. U )   =>    |- ( ph -> ( F supp Z ) = { x e. A | B =/= Z } )
Theorem	extmptsuppeq 6958*	The support of an extended function is the same as the original. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 30-Jun-2019.)
|- ( ph -> B e. W )   &    |- ( ph -> A C_ B )   &    |- ( ( ph /\ n e. ( B \ A ) ) -> X = Z )   =>    |- ( ph -> ( ( n e. A |-> X ) supp Z ) = ( ( n e. B |-> X ) supp Z ) )
Theorem	suppfnss 6959*	The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019.)
|- ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> ( A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) -> ( F supp Z ) C_ ( G supp Z ) ) )
Theorem	funsssuppss 6960	The support of a function which is a subset of another function is a subset of the support of this other function. (Contributed by AV, 27-Jul-2019.)
|- ( ( Fun G /\ F C_ G /\ G e. V ) -> ( F supp Z ) C_ ( G supp Z ) )
Theorem	fnsuppres 6961	Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015.) (Revised by AV, 28-May-2019.)
|- ( ( F Fn ( A u. B ) /\ ( F e. W /\ Z e. V ) /\ ( A i^i B ) = (/) ) -> ( ( F supp Z ) C_ A <-> ( F |` B ) = ( B X. { Z } ) ) )
Theorem	fnsuppeq0 6962	The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 28-May-2019.)
|- ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F supp Z ) = (/) <-> F = ( A X. { Z } ) ) )
Theorem	fczsupp0 6963	The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019.)
|- ( ( B X. { Z } ) supp Z ) = (/)
Theorem	suppss 6964*	Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.)
|- ( ph -> F : A --> B )   &    |- ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )   =>    |- ( ph -> ( F supp Z ) C_ W )
Theorem	suppssr 6965	A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.)
|- ( ph -> F : A --> B )   &    |- ( ph -> ( F supp Z ) C_ W )   &    |- ( ph -> A e. V )   &    |- ( ph -> Z e. U )   =>    |- ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )
Theorem	suppssov1 6966*	Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.)
|- ( ph -> ( ( x e. D |-> A ) supp Y ) C_ L )   &    |- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )   &    |- ( ( ph /\ x e. D ) -> A e. V )   &    |- ( ( ph /\ x e. D ) -> B e. R )   &    |- ( ph -> Y e. W )   =>    |- ( ph -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L )
Theorem	suppssof1 6967*	Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.)
|- ( ph -> ( A supp Y ) C_ L )   &    |- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )   &    |- ( ph -> A : D --> V )   &    |- ( ph -> B : D --> R )   &    |- ( ph -> D e. W )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( ( A oF O B ) supp Z ) C_ L )
Theorem	suppss2 6968*	Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 22-Mar-2015.) (Revised by AV, 28-May-2019.)
|- ( ( ph /\ k e. ( A \ W ) ) -> B = Z )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( ( k e. A |-> B ) supp Z ) C_ W )
Theorem	suppsssn 6969*	Show that the support of a function is a subset of a singleton. (Contributed by AV, 21-Jul-2019.)
|- ( ( ph /\ k e. A /\ k =/= W ) -> B = Z )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( ( k e. A |-> B ) supp Z ) C_ { W } )
Theorem	suppssfv 6970*	Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.)
|- ( ph -> ( ( x e. D |-> A ) supp Y ) C_ L )   &    |- ( ph -> ( F ` Y ) = Z )   &    |- ( ( ph /\ x e. D ) -> A e. V )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( ( x e. D |-> ( F ` A ) ) supp Z ) C_ L )
Theorem	suppofss1d 6971*	Condition for the support of a function operation to be a subset of the support of the left function term. (Contributed by Thierry Arnoux, 21-Jun-2019.)
|- ( ph -> A e. V )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> G : A --> B )   &    |- ( ( ph /\ x e. B ) -> ( Z X x ) = Z )   =>    |- ( ph -> ( ( F oF X G ) supp Z ) C_ ( F supp Z ) )
Theorem	suppofss2d 6972*	Condition for the support of a function operation to be a subset of the support of the right function term. (Contributed by Thierry Arnoux, 21-Jun-2019.)
|- ( ph -> A e. V )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> G : A --> B )   &    |- ( ( ph /\ x e. B ) -> ( x X Z ) = Z )   =>    |- ( ph -> ( ( F oF X G ) supp Z ) C_ ( G supp Z ) )
Theorem	supp0cosupp0 6973	The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019.)
|- ( ( F e. V /\ G e. W ) -> ( ( F supp Z ) = (/) -> ( ( F o. G ) supp Z ) = (/) ) )
Theorem	imacosupp 6974	The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019.)
|- ( ( F e. V /\ G e. W ) -> ( ( Fun G /\ ( F supp Z ) C_ ran G ) -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) ) )
2.4.9  Special "Maps to" operations The following theorems are about maps-to operations (see df-mpt2 6313) 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 "mpt2x" are used (since "x" usually denotes the first argument). This is in line with the currently used conventions for such cases (see cbvmpt2x 6388, ovmpt2x 6444 and fmpt2x 6878). 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	opeliunxp2f 6975*	Membership in a union of Cartesian products, using bound-variable hypothesis for E instead of distinct variable conditions as in opeliunxp2 4978. (Contributed by AV, 25-Oct-2020.)
|- F/_ x E   &    |- ( x = C -> B = E )   =>    |- ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )
Theorem	mpt2xeldm 6976*	If there is an element of the value of an operation given by a maps-to rule, then the first argument is an element of the first component of the domain and the second argument is an element of the second component of the domain depending on the first argument. (Contributed by AV, 25-Oct-2020.)
|- F = ( x e. C , y e. D |-> R )   =>    |- ( N e. ( X F Y ) -> ( X e. C /\ Y e. [_ X / x ]_ D ) )
Theorem	mpt2xneldm 6977*	If the first argument of an operation given by a maps-to rule is not an element of the first component of the domain or the second argument is not an element of the second component of the domain depending on the first argument, then the value of the operation is the empty set. (Contributed by AV, 25-Oct-2020.)
|- F = ( x e. C , y e. D |-> R )   =>    |- ( ( X e/ C \/ Y e/ [_ X / x ]_ D ) -> ( X F Y ) = (/) )
Theorem	mpt2xopn0yelv 6978*	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	mpt2xopynvov0g 6979*	If the second argument 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 is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
|- F = ( x e. _V , y e. ( 1st ` x ) |-> C )   =>    |- ( ( ( V e. X /\ W e. Y ) /\ K e/ V ) -> ( <. V , W >. F K ) = (/) )
Theorem	mpt2xopxnop0 6980*	If the first argument 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, is not an ordered pair, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
|- F = ( x e. _V , y e. ( 1st ` x ) |-> C )   =>    |- ( -. V e. ( _V X. _V ) -> ( V F K ) = (/) )
Theorem	mpt2xopx0ov0 6981*	If the first argument 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, is the empty set, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
|- F = ( x e. _V , y e. ( 1st ` x ) |-> C )   =>    |- ( (/) F K ) = (/)
Theorem	mpt2xopxprcov0 6982*	If the components of the first argument 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, are not sets, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
|- F = ( x e. _V , y e. ( 1st ` x ) |-> C )   =>    |- ( -. ( V e. _V /\ W e. _V ) -> ( <. V , W >. F K ) = (/) )
Theorem	mpt2xopynvov0 6983*	If the second argument 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 is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
|- F = ( x e. _V , y e. ( 1st ` x ) |-> C )   =>    |- ( K e/ V -> ( <. V , W >. F K ) = (/) )
Theorem	mpt2xopoveq 6984*	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 6985*	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	mpt2xopoveqd 6986*	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, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
|- F = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | ph } )   &    |- ( ps -> ( V e. X /\ W e. Y ) )   &    |- ( ( ps /\ -. K e. V ) -> { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } = (/) )   =>    |- ( ps -> ( <. V , W >. F K ) = { n e. V | [. <. V , W >. / x ]. [. K / y ]. ph } )
Theorem	brovex 6987*	A binary relation of the value of an operation given by the "maps to" notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.)
|- O = ( x e. _V , y e. _V |-> C )   &    |- ( ( V e. _V /\ E e. _V ) -> Rel ( V O E ) )   =>    |- ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) )
Theorem	brovmpt2ex 6988*	A binary relation of the value of an operation given by the "maps to" notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.)
|- O = ( x e. _V , y e. _V |-> { <. z , w >. | ph } )   =>    |- ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) )
Theorem	sprmpt2d 6989*	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.) (Revised by AV, 20-Jun-2019.)
|- M = ( v e. _V , e e. _V |-> { <. x , y >. | ( x ( v R e ) y /\ ch ) } )   &    |- ( ( ph /\ v = V /\ e = E ) -> ( ch <-> ps ) )   &    |- ( ph -> ( V e. _V /\ E e. _V ) )   &    |- ( ph -> A. x A. y ( x ( V R E ) y -> th ) )   &    |- ( ph -> { <. x , y >. | th } e. _V )   =>    |- ( ph -> ( V M E ) = { <. x , y >. | ( x ( V R E ) y /\ ps ) } )
2.4.10  Function transposition
Syntax	ctpos 6990	The transposition of a function.
class tpos F
Definition	df-tpos 6991*	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 6992	Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( F C_ G -> tpos F C_ tpos G )
Theorem	tposeq 6993	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( F = G -> tpos F = tpos G )
Theorem	tposeqd 6994	Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> F = G )   =>    |- ( ph -> tpos F = tpos G )
Theorem	tposssxp 6995	The transposition is a subset of a Cartesian product. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F )
Theorem	reltpos 6996	The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- Rel tpos F
Theorem	brtpos2 6997	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 6998	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). This allows us to eliminate sethood hypotheses on A , B in brtpos 7000. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( A e. V -> ( (/)tpos F A <-> (/) F A ) )
Theorem	reldmtpos 6999	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	brtpos 7000	The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( C e. V -> ( <. A , B >.tpos F C <-> <. B , A >. F C ) )