P. 395 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39401-39500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	inmap 39401	Intersection of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   =>    |- ( ph -> ( ( A ^m C ) i^i ( B ^m C ) ) = ( ( A i^i B ) ^m C ) )
Theorem	fcoss 39402	Composition of two mappings. Similar to fco 6058, but with a weaker condition on the domain of F. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F : A --> B )   &    |- ( ph -> C C_ A )   &    |- ( ph -> G : D --> C )   =>    |- ( ph -> ( F o. G ) : D --> B )
Theorem	fsneqrn 39403	Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- B = { A }   &    |- ( ph -> F Fn B )   &    |- ( ph -> G Fn B )   =>    |- ( ph -> ( F = G <-> ( F ` A ) e. ran G ) )
Theorem	difmapsn 39404	Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   =>    |- ( ph -> ( ( A ^m { C } ) \ ( B ^m { C } ) ) = ( ( A \ B ) ^m { C } ) )
Theorem	mapssbi 39405	Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   &    |- ( ph -> C =/= (/) )   =>    |- ( ph -> ( A C_ B <-> ( A ^m C ) C_ ( B ^m C ) ) )
Theorem	unirnmapsn 39406	Equality theorem for a subset of a set exponentiation, where the exponent is a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- C = { A }   &    |- ( ph -> X C_ ( B ^m C ) )   =>    |- ( ph -> X = ( ran U. X ^m C ) )
Theorem	iunmapss 39407*	The indexed union of set exponentiations is a subset of the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   =>    |- ( ph -> U_ x e. A ( B ^m C ) C_ ( U_ x e. A B ^m C ) )
Theorem	ssmapsn 39408*	A subset C of a set exponentiation to a singleton, is its projection D exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/_ f D   &    |- ( ph -> A e. V )   &    |- ( ph -> C C_ ( B ^m { A } ) )   &    |- D = U_ f e. C ran f   =>    |- ( ph -> C = ( D ^m { A } ) )
Theorem	iunmapsn 39409*	The indexed union of set exponentiations to a singleton is equal to the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ph -> C e. Z )   =>    |- ( ph -> U_ x e. A ( B ^m { C } ) = ( U_ x e. A B ^m { C } ) )
Theorem	absfico 39410	Mapping domain and codomain of the absolute value function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- abs : CC --> ( 0 [,) +oo )
Theorem	icof 39411	The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- [,) : ( RR* X. RR* ) --> ~P RR*
Theorem	rnmpt0 39412*	The range of a function in map-to notation is empty if and only if its domain is empty. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- F = ( x e. A |-> B )   =>    |- ( ph -> ( ran F = (/) <-> A = (/) ) )
Theorem	rnmptn0 39413*	The range of a function in map-to notation is nonempty if the domain is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- F = ( x e. A |-> B )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> ran F =/= (/) )
Theorem	elpmrn 39414	The range of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( F e. ( A ^pm B ) -> ran F C_ A )
Theorem	imaexi 39415	The image of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- A e. V   =>    |- ( A " B ) e. _V
Theorem	axccdom 39416*	Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> X ~<_ om )   &    |- ( ( ph /\ z e. X ) -> z =/= (/) )   =>    |- ( ph -> E. f ( f Fn X /\ A. z e. X ( f ` z ) e. z ) )
Theorem	dmmptdf 39417*	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ x ph   &    |- A = ( x e. B |-> C )   &    |- ( ( ph /\ x e. B ) -> C e. V )   =>    |- ( ph -> dom A = B )
Theorem	elpmi2 39418	The domain of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( F e. ( A ^pm B ) -> dom F C_ B )
Theorem	dmrelrnrel 39419*	A relation preserving function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) )   &    |- ( ph -> B e. A )   &    |- ( ph -> C e. A )   &    |- ( ph -> B R C )   =>    |- ( ph -> ( F ` B ) S ( F ` C ) )
Theorem	fdmd 39420	The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> F : A --> B )   =>    |- ( ph -> dom F = A )
Theorem	fco3 39421	Functionality of a composition. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> Fun F )   &    |- ( ph -> Fun G )   =>    |- ( ph -> ( F o. G ) : ( `' G " dom F ) --> ran F )
Theorem	dmexd 39422	The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   =>    |- ( ph -> dom A e. _V )
Theorem	fvcod 39423	Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> Fun G )   &    |- ( ph -> A e. dom G )   &    |- H = ( F o. G )   =>    |- ( ph -> ( H ` A ) = ( F ` ( G ` A ) ) )
Theorem	fcod 39424	Composition of two mappings. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> F : B --> C )   &    |- ( ph -> G : A --> B )   =>    |- ( ph -> ( F o. G ) : A --> C )
Theorem	freld 39425	A mapping is a relation. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> F : A --> B )   =>    |- ( ph -> Rel F )
Theorem	frnd 39426	The range of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> F : A --> B )   =>    |- ( ph -> ran F C_ B )
Theorem	elrnmpt2id 39427*	Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( x e. A /\ y e. B /\ A. x e. A A. y e. B C e. V ) -> ( x F y ) e. ran F )
Theorem	fvmptelrn 39428*	A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> ( x e. A |-> B ) : A --> C )   =>    |- ( ( ph /\ x e. A ) -> B e. C )
Theorem	axccd 39429*	An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A ~~ om )   &    |- ( ( ph /\ x e. A ) -> x =/= (/) )   =>    |- ( ph -> E. f A. x e. A ( f ` x ) e. x )
Theorem	axccd2 39430*	An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A ~<_ om )   &    |- ( ( ph /\ x e. A ) -> x =/= (/) )   =>    |- ( ph -> E. f A. x e. A ( f ` x ) e. x )
Theorem	funimassd 39431*	Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> Fun F )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) e. B )   =>    |- ( ph -> ( F " A ) C_ B )
Theorem	fimassd 39432	The image of a class is a subset of its codomain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F : A --> B )   =>    |- ( ph -> ( F " X ) C_ B )
Theorem	feqresmptf 39433*	Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x F   &    |- ( ph -> F : A --> B )   &    |- ( ph -> C C_ A )   =>    |- ( ph -> ( F |` C ) = ( x e. C |-> ( F ` x ) ) )
Theorem	fnmptd 39434*	The maps-to notation defines a function with domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- F = ( x e. A |-> B )   =>    |- ( ph -> F Fn A )
Theorem	elrnmpt1d 39435	Elementhood in an image set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F = ( x e. A |-> B )   &    |- ( ph -> x e. A )   &    |- ( ph -> B e. V )   =>    |- ( ph -> B e. ran F )
Theorem	dmresss 39436	The domain of a restriction is a subset of the original domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- dom ( A |` B ) C_ dom A
Theorem	mptima 39437*	Image of a function in map-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ( x e. A |-> B ) " C ) = ran ( x e. ( A i^i C ) |-> B )
Theorem	dmmptssf 39438	The domain of a mapping is a subset of its base class. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x A   &    |- F = ( x e. A |-> B )   =>    |- dom F C_ A
Theorem	dmmptdf2 39439	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- F/_ x B   &    |- A = ( x e. B |-> C )   &    |- ( ( ph /\ x e. B ) -> C e. V )   =>    |- ( ph -> dom A = B )
Theorem	dmuz 39440	Domain of the upper integers function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- dom ZZ>= = ZZ
Theorem	fndmd 39441	The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F Fn A )   =>    |- ( ph -> dom F = A )
Theorem	fmptd2f 39442*	Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. C )   =>    |- ( ph -> ( x e. A |-> B ) : A --> C )
Theorem	mpteq1df 39443	An equality theorem for the maps to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A = B )   =>    |- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )
Theorem	mptexf 39444	If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6484. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x A   &    |- A e. _V   =>    |- ( x e. A |-> B ) e. _V
Theorem	fvmptd2 39445*	Deduction version of fvmpt 6282. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F = ( x e. D |-> B )   &    |- ( ( ph /\ x = A ) -> B = C )   &    |- ( ph -> A e. D )   &    |- ( ph -> C e. V )   =>    |- ( ph -> ( F ` A ) = C )
Theorem	fvmpt4 39446*	Value of a function given by the "maps to" notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ( x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B )
Theorem	fvmptd3 39447*	Deduction version of fvmpt 6282. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F = ( x e. D |-> B )   &    |- ( x = A -> B = C )   &    |- ( ph -> A e. D )   &    |- ( ph -> C e. V )   =>    |- ( ph -> ( F ` A ) = C )
Theorem	fmptf 39448*	Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x B   &    |- F = ( x e. A |-> C )   =>    |- ( A. x e. A C e. B <-> F : A --> B )
Theorem	resimass 39449	The image of a restriction is a subset of the original image. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ( A |` B ) " C ) C_ ( A " C )
Theorem	mptssid 39450	The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x A   &    |- C = { x e. A | B e. _V }   =>    |- ( x e. A |-> B ) = ( x e. C |-> B )
Theorem	mptfnd 39451	The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) (Revised by Thierry Arnoux, 10-May-2017.)
|- F/_ x A   &    |- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> ( x e. A |-> B ) Fn A )
Theorem	mpteq12da 39452	An equality inference for the maps to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A = C )   &    |- ( ( ph /\ x e. A ) -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	rnmptlb 39453*	Boundness below of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> E. y e. RR A. x e. A y <_ B )   =>    |- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z )
Theorem	elpreimad 39454	Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F Fn A )   &    |- ( ph -> B e. A )   &    |- ( ph -> ( F ` B ) e. C )   =>    |- ( ph -> B e. ( `' F " C ) )
Theorem	rnmptbddlem 39455*	Boundness of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   =>    |- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )
Theorem	rnmptbdd 39456*	Boundness of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   =>    |- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )
Theorem	mptima2 39457*	Image of a function in map-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> C C_ A )   =>    |- ( ph -> ( ( x e. A |-> B ) " C ) = ran ( x e. C |-> B ) )
Theorem	fvelimad 39458*	Function value in an image. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x F   &    |- ( ph -> F Fn A )   &    |- ( ph -> C e. ( F " B ) )   =>    |- ( ph -> E. x e. ( A i^i B ) ( F ` x ) = C )
Theorem	fnfvimad 39459	A function's value belongs to the image. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F Fn A )   &    |- ( ph -> B e. A )   &    |- ( ph -> B e. C )   =>    |- ( ph -> ( F ` B ) e. ( F " C ) )
Theorem	fmptd2 39460*	Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ( ph /\ x e. A ) -> B e. C )   =>    |- ( ph -> ( x e. A |-> B ) : A --> C )
Theorem	funimaeq 39461*	Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> Fun F )   &    |- ( ph -> Fun G )   &    |- ( ph -> A C_ dom F )   &    |- ( ph -> A C_ dom G )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = ( G ` x ) )   =>    |- ( ph -> ( F " A ) = ( G " A ) )
Theorem	rnmptssf 39462*	The range of an operation given by the "maps to" notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x C   &    |- F = ( x e. A |-> B )   =>    |- ( A. x e. A B e. C -> ran F C_ C )
Theorem	rnmptbd2lem 39463*	Boundness below of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> ( E. y e. RR A. x e. A y <_ B <-> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z ) )
Theorem	rnmptbd2 39464*	Boundness below of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> ( E. y e. RR A. x e. A y <_ B <-> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z ) )
Theorem	infnsuprnmpt 39465*	The indexed infimum of real numbers is the negative of the indexed supremum of the negative values. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A y <_ B )   =>    |- ( ph -> inf ( ran ( x e. A |-> B ) , RR , < ) = -u sup ( ran ( x e. A |-> -u B ) , RR , < ) )
Theorem	suprclrnmpt 39466*	Closure of the indexed supremum of a nonempty bounded set of reals. Range of a function in map-to notation can be used, to express an indexed supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   =>    |- ( ph -> sup ( ran ( x e. A |-> B ) , RR , < ) e. RR )
Theorem	suprubrnmpt2 39467*	A member of a nonempty indexed set of reals is less than or equal to the set's upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   &    |- ( ph -> C e. A )   &    |- ( ph -> D e. RR )   &    |- ( x = C -> B = D )   =>    |- ( ph -> D <_ sup ( ran ( x e. A |-> B ) , RR , < ) )
Theorem	suprubrnmpt 39468*	A member of a nonempty indexed set of reals is less than or equal to the set's upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   =>    |- ( ( ph /\ x e. A ) -> B <_ sup ( ran ( x e. A |-> B ) , RR , < ) )
Theorem	rnmptssdf 39469*	The range of an operation given by the "maps to" notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- F/_ x C   &    |- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. C )   =>    |- ( ph -> ran F C_ C )
Theorem	rnmptbdlem 39470*	Boundness above of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> ( E. y e. RR A. x e. A B <_ y <-> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) )
Theorem	rnmptbd 39471*	Boundness above of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> ( E. y e. RR A. x e. A B <_ y <-> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) )
Theorem	rnmptss2 39472*	The range of an operation given by the "maps to" notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A C_ B )   &    |- ( ( ph /\ x e. A ) -> C e. V )   =>    |- ( ph -> ran ( x e. A |-> C ) C_ ran ( x e. B |-> C ) )
Theorem	elmptima 39473*	The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( C e. V -> ( C e. ( ( x e. A |-> B ) " D ) <-> E. x e. ( A i^i D ) C = B ) )
Theorem	ralrnmpt3 39474*	A restricted quantifier over an image set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. y e. ran ( x e. A |-> B ) ps <-> A. x e. A ch ) )
Theorem	fvelima2 39475*	Function value in an image. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ( F Fn A /\ B e. ( F " C ) ) -> E. x e. ( A i^i C ) ( F ` x ) = B )
Theorem	funresd 39476	A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> Fun F )   =>    |- ( ph -> Fun ( F |` A ) )
Theorem	rnmptssbi 39477*	The range of an operation given by the "maps to" notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> ( ran F C_ C <-> A. x e. A B e. C ) )
Theorem	fnfvima2 39478	Given an element of the preimage, its function value is in the image. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> F Fn A )   &    |- ( ph -> B e. A )   &    |- ( ph -> B e. C )   =>    |- ( ph -> ( F ` B ) e. ( F " C ) )
Theorem	fnfvelrnd 39479	A function's value belongs to its range. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> F Fn A )   &    |- ( ph -> B e. A )   =>    |- ( ph -> ( F ` B ) e. ran F )
Theorem	imass2d 39480	Subset theorem for image. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( C " A ) C_ ( C " B ) )
Theorem	imassmpt 39481*	Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- ( ( ph /\ x e. ( A i^i C ) ) -> B e. V )   &    |- F = ( x e. A |-> B )   =>    |- ( ph -> ( ( F " C ) C_ D <-> A. x e. ( A i^i C ) B e. D ) )
Theorem	fnssresd 39482	Restriction of a function to a subclass of its domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> F Fn A )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( F |` B ) Fn B )
Theorem	fpmd 39483	A total function is a partial function. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C C_ A )   &    |- ( ph -> F : C --> B )   =>    |- ( ph -> F e. ( B ^pm A ) )
Theorem	fconst7 39484*	An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- F/ x ph   &    |- F/_ x F   &    |- ( ph -> F Fn A )   &    |- ( ph -> B e. V )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )   =>    |- ( ph -> F = ( A X. { B } ) )
20.32.3  Ordering on real numbers - Real and complex numbers basic operations
Theorem	sub2times 39485	Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. CC -> ( A - ( 2 x. A ) ) = -u A )
Theorem	xrltled 39486	'Less than' implies 'less than or equal to', for extended reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> A <_ B )
Theorem	abssubrp 39487	The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. CC /\ B e. CC /\ A =/= B ) -> ( abs ` ( A - B ) ) e. RR+ )
Theorem	elfzfzo 39488	Relationship between membership in a half open finite set of sequential integers and membership in a finite set of sequential intergers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. ( M..^ N ) <-> ( A e. ( M ... N ) /\ A < N ) )
Theorem	oddfl 39489	Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> K = ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) )
Theorem	abscosbd 39490	Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> ( abs ` ( cos ` A ) ) <_ 1 )
Theorem	mul13d 39491	Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A x. ( B x. C ) ) = ( C x. ( B x. A ) ) )
Theorem	negpilt0 39492	Negative pi is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- -u pi < 0
Theorem	dstregt0 39493*	A complex number A that is not real, has a distance from the reals that is strictly larger than 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. ( CC \ RR ) )   =>    |- ( ph -> E. x e. RR+ A. y e. RR x < ( abs ` ( A - y ) ) )
Theorem	subadd4b 39494	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A - B ) + ( C - D ) ) = ( ( A - D ) + ( C - B ) ) )
Theorem	xrlttri5d 39495	Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A =/= B )   &    |- ( ph -> -. B < A )   =>    |- ( ph -> A < B )
Theorem	neglt 39496	The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR+ -> -u A < A )
Theorem	zltlesub 39497	If an integer N is smaller or equal to a real, and we subtract a quantity smaller than 1, then N is smaller or equal to the result. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> N e. ZZ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> N <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> B < 1 )   &    |- ( ph -> ( A - B ) e. ZZ )   =>    |- ( ph -> N <_ ( A - B ) )
Theorem	divlt0gt0d 39498	The ratio of a negative numerator and a positive denominator is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> A < 0 )   =>    |- ( ph -> ( A / B ) < 0 )
Theorem	subsub23d 39499	Swap subtrahend and result of subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = C <-> ( A - C ) = B ) )
Theorem	2timesgt 39500	Double of a positive real is larger than the real itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR+ -> A < ( 2 x. A ) )