P. 336 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33501-33600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	areacirclem2 33501*	Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
|- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
Theorem	areacirclem3 33502*	Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
|- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( 2 x. ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. L^1 )
Theorem	areacirclem4 33503*	Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
|- ( R e. RR+ -> ( t e. ( -u R [,] R ) |-> ( ( R ^ 2 ) x. ( (arcsin ` ( t / R ) ) + ( ( t / R ) x. ( sqr ` ( 1 - ( ( t / R ) ^ 2 ) ) ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
Theorem	areacirclem5 33504*	Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
|- S = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) }   =>    |- ( ( R e. RR /\ 0 <_ R /\ t e. RR ) -> ( S " { t } ) = if ( ( abs ` t ) <_ R , ( -u ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) [,] ( sqr ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) , (/) ) )
Theorem	areacirc 33505*	The area of a circle of radius R is pi x. R ^ 2. This is Metamath 100 proof #9. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
|- S = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) <_ ( R ^ 2 ) ) }   =>    |- ( ( R e. RR /\ 0 <_ R ) -> (area ` S ) = ( pi x. ( R ^ 2 ) ) )
20.19  Mathbox for Jeff Madsen
20.19.1  Logic and set theory
Theorem	anim12da 33506	Conjoin antecedents and consequents in a deduction. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- ( ( ph /\ ps ) -> th )   &    |- ( ( ph /\ ch ) -> ta )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> ( th /\ ta ) )
Theorem	unirep 33507*	Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011.)
|- ( y = D -> ( ph <-> ps ) )   &    |- ( y = D -> B = C )   &    |- ( y = z -> ( ph <-> ch ) )   &    |- ( y = z -> B = F )   &    |- B e. _V   =>    |- ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> ( iota x E. y e. A ( ph /\ x = B ) ) = C )
Theorem	cover2 33508*	Two ways of expressing the statement "there is a cover of A by elements of B such that for each set in the cover, ph." Note that ph and x must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010.)
|- B e. _V   &    |- A = U. B   =>    |- ( A. x e. A E. y e. B ( x e. y /\ ph ) <-> E. z e. ~P B ( U. z = A /\ A. y e. z ph ) )
Theorem	cover2g 33509*	Two ways of expressing the statement "there is a cover of A by elements of B such that for each set in the cover, ph." Note that ph and x must be distinct. (Contributed by Jeff Madsen, 21-Jun-2010.)
|- A = U. B   =>    |- ( B e. C -> ( A. x e. A E. y e. B ( x e. y /\ ph ) <-> E. z e. ~P B ( U. z = A /\ A. y e. z ph ) ) )
Theorem	brabg2 33510*	Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- R = { <. x , y >. | ph }   &    |- ( ch -> A e. C )   =>    |- ( B e. D -> ( A R B <-> ch ) )
Theorem	opelopab3 33511*	Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- ( ch -> A e. C )   =>    |- ( B e. D -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )
Theorem	cocanfo 33512	Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
|- ( ( ( F : A -onto-> B /\ G Fn B /\ H Fn B ) /\ ( G o. F ) = ( H o. F ) ) -> G = H )
Theorem	brresi 33513	Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- B e. _V   =>    |- ( A ( R |` C ) B -> A R B )
Theorem	fnopabeqd 33514*	Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ( ph -> B = C )   =>    |- ( ph -> { <. x , y >. | ( x e. A /\ y = B ) } = { <. x , y >. | ( x e. A /\ y = C ) } )
Theorem	fvopabf4g 33515*	Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- C e. _V   &    |- ( x = A -> B = C )   &    |- F = ( x e. ( R ^m D ) |-> B )   =>    |- ( ( D e. X /\ R e. Y /\ A : D --> R ) -> ( F ` A ) = C )
Theorem	eqfnun 33516	Two functions on A u. B are equal if and only if they have equal restrictions to both A and B. (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ( ( F Fn ( A u. B ) /\ G Fn ( A u. B ) ) -> ( F = G <-> ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) ) )
Theorem	fnopabco 33517*	Composition of a function with a function abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- ( x e. A -> B e. C )   &    |- F = { <. x , y >. | ( x e. A /\ y = B ) }   &    |- G = { <. x , y >. | ( x e. A /\ y = ( H ` B ) ) }   =>    |- ( H Fn C -> G = ( H o. F ) )
Theorem	opropabco 33518*	Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.)
|- ( x e. A -> B e. R )   &    |- ( x e. A -> C e. S )   &    |- F = { <. x , y >. | ( x e. A /\ y = <. B , C >. ) }   &    |- G = { <. x , y >. | ( x e. A /\ y = ( B M C ) ) }   =>    |- ( M Fn ( R X. S ) -> G = ( M o. F ) )
Theorem	f1opr 33519*	Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( F : ( A X. B ) -1-1-> C <-> ( F : ( A X. B ) --> C /\ A. r e. A A. s e. B A. t e. A A. u e. B ( ( r F s ) = ( t F u ) -> ( r = t /\ s = u ) ) ) )
Theorem	cocnv 33520	Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( Fun F /\ Fun G ) -> ( ( F o. G ) o. `' G ) = ( F |` ran G ) )
Theorem	f1ocan1fv 33521	Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
|- ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. B ) -> ( ( F o. G ) ` ( `' G ` X ) ) = ( F ` X ) )
Theorem	f1ocan2fv 33522	Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( Fun F /\ G : A -1-1-onto-> B /\ X e. A ) -> ( ( F o. `' G ) ` ( G ` X ) ) = ( F ` X ) )
Theorem	inixp 33523*	Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( X_ x e. A B i^i X_ x e. A C ) = X_ x e. A ( B i^i C )
Theorem	upixp 33524*	Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- X = X_ b e. A ( C ` b )   &    |- P = ( w e. A |-> ( x e. X |-> ( x ` w ) ) )   =>    |- ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> E! h ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) )
Theorem	abrexdom 33525*	An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( y e. A -> E* x ph )   =>    |- ( A e. V -> { x | E. y e. A ph } ~<_ A )
Theorem	abrexdom2 33526*	An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. V -> { x | E. y e. A x = B } ~<_ A )
Theorem	ac6gf 33527*	Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- F/ y ps   &    |- ( y = ( f ` x ) -> ( ph <-> ps ) )   =>    |- ( ( A e. C /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )
Theorem	indexa 33528*	If for every element of an indexing set A there exists a corresponding element of another set B, then there exists a subset of B consisting only of those elements which are indexed by A. Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( B e. M /\ A. x e. A E. y e. B ph ) -> E. c ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) )
Theorem	indexdom 33529*	If for every element of an indexing set A there exists a corresponding element of another set B, then there exists a subset of B consisting only of those elements which are indexed by A, and which is dominated by the set A. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( A e. M /\ A. x e. A E. y e. B ph ) -> E. c ( ( c ~<_ A /\ c C_ B ) /\ ( A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) ) )
Theorem	frinfm 33530*	A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( R Fr A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )
Theorem	welb 33531*	A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( R We A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> ( `' R Or B /\ E. x e. B ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) ) )
Theorem	supex2g 33532	Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. C -> sup ( B , A , R ) e. _V )
Theorem	supclt 33533*	Closure of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( R Or A /\ E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) -> sup ( B , A , R ) e. A )
Theorem	supubt 33534*	Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( R Or A /\ E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) -> ( C e. B -> -. sup ( B , A , R ) R C ) )
20.19.2  Real and complex numbers; integers
Theorem	filbcmb 33535*	Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( A e. Fin /\ A =/= (/) /\ B C_ RR ) -> ( A. x e. A E. y e. B A. z e. B ( y <_ z -> ph ) -> E. y e. B A. z e. B ( y <_ z -> A. x e. A ph ) ) )
Theorem	rdr 33536	Two ways of expressing the remainder when A is divided by B. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( A mod B ) ) / B ) = ( |_ ` ( A / B ) ) )
Theorem	fzmul 33537	Membership of a product in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. NN ) -> ( J e. ( M ... N ) -> ( K x. J ) e. ( ( K x. M ) ... ( K x. N ) ) ) )
20.19.3  Sequences and sums
Theorem	sdclem2 33538*	Lemma for sdc 33540. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- Z = ( ZZ>= ` M )   &    |- ( g = ( f |` ( M ... n ) ) -> ( ps <-> ch ) )   &    |- ( n = M -> ( ps <-> ta ) )   &    |- ( n = k -> ( ps <-> th ) )   &    |- ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. g ( g : { M } --> A /\ ta ) )   &    |- ( ( ph /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )   &    |- J = { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) }   &    |- F = ( w e. Z , x e. J |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )   &    |- F/ k ph   &    |- ( ph -> G : Z --> J )   &    |- ( ph -> ( G ` M ) : ( M ... M ) --> A )   &    |- ( ( ph /\ w e. Z ) -> ( G ` ( w + 1 ) ) e. ( w F ( G ` w ) ) )   =>    |- ( ph -> E. f ( f : Z --> A /\ A. n e. Z ch ) )
Theorem	sdclem1 33539*	Lemma for sdc 33540. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- Z = ( ZZ>= ` M )   &    |- ( g = ( f |` ( M ... n ) ) -> ( ps <-> ch ) )   &    |- ( n = M -> ( ps <-> ta ) )   &    |- ( n = k -> ( ps <-> th ) )   &    |- ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. g ( g : { M } --> A /\ ta ) )   &    |- ( ( ph /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )   &    |- J = { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) }   &    |- F = ( w e. Z , x e. J |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )   =>    |- ( ph -> E. f ( f : Z --> A /\ A. n e. Z ch ) )
Theorem	sdc 33540*	Strong dependent choice. Suppose we may choose an element of A such that property ps holds, and suppose that if we have already chosen the first k elements (represented here by a function from 1 ... k to A), we may choose another element so that all k + 1 elements taken together have property ps. Then there exists an infinite sequence of elements of A such that the first n terms of this sequence satisfy ps for all n. This theorem allows us to construct infinite seqeunces where each term depends on all the previous terms in the sequence. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 3-Jun-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( g = ( f |` ( M ... n ) ) -> ( ps <-> ch ) )   &    |- ( n = M -> ( ps <-> ta ) )   &    |- ( n = k -> ( ps <-> th ) )   &    |- ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. g ( g : { M } --> A /\ ta ) )   &    |- ( ( ph /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )   =>    |- ( ph -> E. f ( f : Z --> A /\ A. n e. Z ch ) )
Theorem	fdc 33541*	Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice. (Contributed by Jeff Madsen, 18-Jun-2010.)
|- A e. _V   &    |- M e. ZZ   &    |- Z = ( ZZ>= ` M )   &    |- N = ( M + 1 )   &    |- ( a = ( f ` ( k - 1 ) ) -> ( ph <-> ps ) )   &    |- ( b = ( f ` k ) -> ( ps <-> ch ) )   &    |- ( a = ( f ` n ) -> ( th <-> ta ) )   &    |- ( et -> C e. A )   &    |- ( et -> R Fr A )   &    |- ( ( et /\ a e. A ) -> ( th \/ E. b e. A ph ) )   &    |- ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> b R a )   =>    |- ( et -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = C /\ ta ) /\ A. k e. ( N ... n ) ch ) )
Theorem	fdc1 33542*	Variant of fdc 33541 with no specified base value. (Contributed by Jeff Madsen, 18-Jun-2010.)
|- A e. _V   &    |- M e. ZZ   &    |- Z = ( ZZ>= ` M )   &    |- N = ( M + 1 )   &    |- ( a = ( f ` M ) -> ( ze <-> si ) )   &    |- ( a = ( f ` ( k - 1 ) ) -> ( ph <-> ps ) )   &    |- ( b = ( f ` k ) -> ( ps <-> ch ) )   &    |- ( a = ( f ` n ) -> ( th <-> ta ) )   &    |- ( et -> E. a e. A ze )   &    |- ( et -> R Fr A )   &    |- ( ( et /\ a e. A ) -> ( th \/ E. b e. A ph ) )   &    |- ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> b R a )   =>    |- ( et -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) )
Theorem	seqpo 33543*	Two ways to say that a sequence respects a partial order. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( R Po A /\ F : NN --> A ) -> ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) <-> A. m e. NN A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) ) )
Theorem	incsequz 33544*	An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) /\ A e. NN ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` A ) )
Theorem	incsequz2 33545*	An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) /\ A e. NN ) -> E. n e. NN A. k e. ( ZZ>= ` n ) ( F ` k ) e. ( ZZ>= ` A ) )
Theorem	nnubfi 33546*	A bounded above set of positive integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.)
|- ( ( A C_ NN /\ B e. NN ) -> { x e. A | x < B } e. Fin )
Theorem	nninfnub 33547*	An infinite set of positive integers is unbounded above. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.)
|- ( ( A C_ NN /\ -. A e. Fin /\ B e. NN ) -> { x e. A | B < x } =/= (/) )
20.19.4  Topology
Theorem	subspopn 33548	An open set is open in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A ) ) -> B e. ( J ↾t A ) )
Theorem	neificl 33549	Neighborhoods are closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Nov-2013.)
|- ( ( ( J e. Top /\ N C_ ( ( nei ` J ) ` S ) ) /\ ( N e. Fin /\ N =/= (/) ) ) -> |^| N e. ( ( nei ` J ) ` S ) )
Theorem	lpss2 33550	Limit points of a subset are limit points of the larger set. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( limPt ` J ) ` B ) C_ ( ( limPt ` J ) ` A ) )
20.19.5  Metric spaces
Theorem	metf1o 33551*	Use a bijection with a metric space to construct a metric on a set. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- N = ( x e. Y , y e. Y |-> ( ( F ` x ) M ( F ` y ) ) )   =>    |- ( ( Y e. A /\ M e. ( Met ` X ) /\ F : Y -1-1-onto-> X ) -> N e. ( Met ` Y ) )
Theorem	blssp 33552	A ball in the subspace metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jan-2014.)
|- N = ( M |` ( S X. S ) )   =>    |- ( ( ( M e. ( Met ` X ) /\ S C_ X ) /\ ( Y e. S /\ R e. RR+ ) ) -> ( Y ( ball ` N ) R ) = ( ( Y ( ball ` M ) R ) i^i S ) )
Theorem	mettrifi 33553*	Generalized triangle inequality for arbitrary finite sums. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. X )   =>    |- ( ph -> ( ( F ` M ) D ( F ` N ) ) <_ sum_ k e. ( M ... ( N - 1 ) ) ( ( F ` k ) D ( F ` ( k + 1 ) ) ) )
Theorem	lmclim2 33554*	A sequence in a metric space converges to a point iff the distance between the point and the elements of the sequence converges to 0. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
|- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> F : NN --> X )   &    |- J = ( MetOpen ` D )   &    |- G = ( x e. NN |-> ( ( F ` x ) D Y ) )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> ( F ( ~~> t ` J ) Y <-> G ~~> 0 ) )
Theorem	geomcau 33555*	If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
|- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> F : NN --> X )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> B < 1 )   &    |- ( ( ph /\ k e. NN ) -> ( ( F ` k ) D ( F ` ( k + 1 ) ) ) <_ ( A x. ( B ^ k ) ) )   =>    |- ( ph -> F e. ( Cau ` D ) )
Theorem	caures 33556	The restriction of a Cauchy sequence to an upper set of integers is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> F e. ( X ^pm CC ) )   =>    |- ( ph -> ( F e. ( Cau ` D ) <-> ( F |` Z ) e. ( Cau ` D ) ) )
Theorem	caushft 33557*	A shifted Cauchy sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- W = ( ZZ>= ` ( M + N ) )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` ( k + N ) ) )   &    |- ( ph -> F e. ( Cau ` D ) )   &    |- ( ph -> G : W --> X )   =>    |- ( ph -> G e. ( Cau ` D ) )
20.19.6  Continuous maps and homeomorphisms
Theorem	constcncf 33558*	A constant function is a continuous function on CC. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved into main set.mm as cncfmptc 22714 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- F = ( x e. CC |-> A )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	idcncf 33559	The identity function is a continuous function on CC. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 22715 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- F = ( x e. CC |-> x )   =>    |- F e. ( CC -cn-> CC )
Theorem	sub1cncf 33560*	Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- F = ( x e. CC |-> ( x - A ) )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	sub2cncf 33561*	Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- F = ( x e. CC |-> ( A - x ) )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	cnres2 33562*	The restriction of a continuous function to a subset is continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> ( F |` A ) e. ( ( J ↾t A ) Cn ( K ↾t B ) ) )
Theorem	cnresima 33563	A continuous function is continuous onto its image. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( ( J e. Top /\ K e. Top /\ F e. ( J Cn K ) ) -> F e. ( J Cn ( K ↾t ran F ) ) )
Theorem	cncfres 33564*	A continuous function on complex numbers restricted to a subset. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- A C_ CC   &    |- B C_ CC   &    |- F = ( x e. CC |-> C )   &    |- G = ( x e. A |-> C )   &    |- ( x e. A -> C e. B )   &    |- F e. ( CC -cn-> CC )   &    |- J = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) )   &    |- K = ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) )   =>    |- G e. ( J Cn K )
20.19.7  Boundedness
Syntax	ctotbnd 33565	Extend class notation with the class of totally bounded metric spaces.
class TotBnd
Syntax	cbnd 33566	Extend class notation with the class of bounded metric spaces.
class Bnd
Definition	df-totbnd 33567*	Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- TotBnd = ( x e. _V |-> { m e. ( Met ` x ) | A. d e. RR+ E. v e. Fin ( U. v = x /\ A. b e. v E. y e. x b = ( y ( ball ` m ) d ) ) } )
Theorem	istotbnd 33568*	The predicate "is a totally bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( M e. ( TotBnd ` X ) <-> ( M e. ( Met ` X ) /\ A. d e. RR+ E. v e. Fin ( U. v = X /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
Theorem	istotbnd2 33569*	The predicate "is a totally bounded metric space." (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( M e. ( Met ` X ) -> ( M e. ( TotBnd ` X ) <-> A. d e. RR+ E. v e. Fin ( U. v = X /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
Theorem	istotbnd3 33570*	A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015.)
|- ( M e. ( TotBnd ` X ) <-> ( M e. ( Met ` X ) /\ A. d e. RR+ E. v e. ( ~P X i^i Fin ) U_ x e. v ( x ( ball ` M ) d ) = X ) )
Theorem	totbndmet 33571	The predicate "totally bounded" implies M is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( M e. ( TotBnd ` X ) -> M e. ( Met ` X ) )
Theorem	0totbnd 33572	The metric (there is only one) on the empty set is totally bounded. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- ( X = (/) -> ( M e. ( TotBnd ` X ) <-> M e. ( Met ` X ) ) )
Theorem	sstotbnd2 33573*	Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015.)
|- N = ( M |` ( Y X. Y ) )   =>    |- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. ( ~P X i^i Fin ) Y C_ U_ x e. v ( x ( ball ` M ) d ) ) )
Theorem	sstotbnd 33574*	Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- N = ( M |` ( Y X. Y ) )   =>    |- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. Fin ( Y C_ U. v /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
Theorem	sstotbnd3 33575*	Use a net that is not necessarily finite, but for which only finitely many balls meet the subset. (Contributed by Mario Carneiro, 14-Sep-2015.)
|- N = ( M |` ( Y X. Y ) )   =>    |- ( ( M e. ( Met ` X ) /\ Y C_ X ) -> ( N e. ( TotBnd ` Y ) <-> A. d e. RR+ E. v e. ~P X ( Y C_ U_ x e. v ( x ( ball ` M ) d ) /\ { x e. v | ( ( x ( ball ` M ) d ) i^i Y ) =/= (/) } e. Fin ) ) )
Theorem	totbndss 33576	A subset of a totally bounded metric space is totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- ( ( M e. ( TotBnd ` X ) /\ S C_ X ) -> ( M |` ( S X. S ) ) e. ( TotBnd ` S ) )
Theorem	equivtotbnd 33577*	If the metric M is "strongly finer" than N (meaning that there is a positive real constant R such that N ( x , y ) <_ R x. M ( x , y )), then total boundedness of M implies total boundedness of N. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is totally bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.)
|- ( ph -> M e. ( TotBnd ` X ) )   &    |- ( ph -> N e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )   =>    |- ( ph -> N e. ( TotBnd ` X ) )
Definition	df-bnd 33578*	Define the class of bounded metrics. A metric space is bounded iff it can be covered by a single ball. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- Bnd = ( x e. _V |-> { m e. ( Met ` x ) | A. y e. x E. r e. RR+ x = ( y ( ball ` m ) r ) } )
Theorem	isbnd 33579*	The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) )
Theorem	bndmet 33580	A bounded metric space is a metric space. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- ( M e. ( Bnd ` X ) -> M e. ( Met ` X ) )
Theorem	isbndx 33581*	A "bounded extended metric" (meaning that it satisfies the same condition as a bounded metric, but with "metric" replaced with "extended metric") is a metric and thus is bounded in the conventional sense. (Contributed by Mario Carneiro, 12-Sep-2015.)
|- ( M e. ( Bnd ` X ) <-> ( M e. ( *Met ` X ) /\ A. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) )
Theorem	isbnd2 33582*	The predicate "is a bounded metric space". Uses a single point instead of an arbitrary point in the space. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( M e. ( Bnd ` X ) /\ X =/= (/) ) <-> ( M e. ( *Met ` X ) /\ E. x e. X E. r e. RR+ X = ( x ( ball ` M ) r ) ) )
Theorem	isbnd3 33583*	A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015.)
|- ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ E. x e. RR M : ( X X. X ) --> ( 0 [,] x ) ) )
Theorem	isbnd3b 33584*	A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ E. x e. RR A. y e. X A. z e. X ( y M z ) <_ x ) )
Theorem	bndss 33585	A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( M e. ( Bnd ` X ) /\ S C_ X ) -> ( M |` ( S X. S ) ) e. ( Bnd ` S ) )
Theorem	blbnd 33586	A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 15-Jan-2014.)
|- ( ( M e. ( *Met ` X ) /\ Y e. X /\ R e. RR ) -> ( M |` ( ( Y ( ball ` M ) R ) X. ( Y ( ball ` M ) R ) ) ) e. ( Bnd ` ( Y ( ball ` M ) R ) ) )
Theorem	ssbnd 33587*	A subset of a metric space is bounded iff it is contained in a ball around P, for any P in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015.)
|- N = ( M |` ( Y X. Y ) )   =>    |- ( ( M e. ( Met ` X ) /\ P e. X ) -> ( N e. ( Bnd ` Y ) <-> E. d e. RR Y C_ ( P ( ball ` M ) d ) ) )
Theorem	totbndbnd 33588	A totally bounded metric space is bounded. This theorem fails for extended metrics - a bounded extended metric is a metric, but there are totally bounded extended metrics that are not metrics (if we were to weaken istotbnd 33568 to only require that M be an extended metric). A counterexample is the discrete extended metric (assigning distinct points distance +oo) on a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- ( M e. ( TotBnd ` X ) -> M e. ( Bnd ` X ) )
Theorem	equivbnd 33589*	If the metric M is "strongly finer" than N (meaning that there is a positive real constant R such that N ( x , y ) <_ R x. M ( x , y )), then boundedness of M implies boundedness of N. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.)
|- ( ph -> M e. ( Bnd ` X ) )   &    |- ( ph -> N e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )   =>    |- ( ph -> N e. ( Bnd ` X ) )
Theorem	bnd2lem 33590	Lemma for equivbnd2 33591 and similar theorems. (Contributed by Jeff Madsen, 16-Sep-2015.)
|- D = ( M |` ( Y X. Y ) )   =>    |- ( ( M e. ( Met ` X ) /\ D e. ( Bnd ` Y ) ) -> Y C_ X )
Theorem	equivbnd2 33591*	If balls are totally bounded in the metric M, then balls are totally bounded in the equivalent metric N. (Contributed by Mario Carneiro, 15-Sep-2015.)
|- ( ph -> M e. ( Met ` X ) )   &    |- ( ph -> N e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> S e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x N y ) <_ ( R x. ( x M y ) ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x M y ) <_ ( S x. ( x N y ) ) )   &    |- C = ( M |` ( Y X. Y ) )   &    |- D = ( N |` ( Y X. Y ) )   &    |- ( ph -> ( C e. ( TotBnd ` Y ) <-> C e. ( Bnd ` Y ) ) )   =>    |- ( ph -> ( D e. ( TotBnd ` Y ) <-> D e. ( Bnd ` Y ) ) )
Theorem	prdsbnd 33592*	The product metric over finite index set is bounded if all the factors are bounded. (Contributed by Mario Carneiro, 13-Sep-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- V = ( Base ` ( R ` x ) )   &    |- E = ( ( dist ` ( R ` x ) ) |` ( V X. V ) )   &    |- D = ( dist ` Y )   &    |- ( ph -> S e. W )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R Fn I )   &    |- ( ( ph /\ x e. I ) -> E e. ( Bnd ` V ) )   =>    |- ( ph -> D e. ( Bnd ` B ) )
Theorem	prdstotbnd 33593*	The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- V = ( Base ` ( R ` x ) )   &    |- E = ( ( dist ` ( R ` x ) ) |` ( V X. V ) )   &    |- D = ( dist ` Y )   &    |- ( ph -> S e. W )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R Fn I )   &    |- ( ( ph /\ x e. I ) -> E e. ( TotBnd ` V ) )   =>    |- ( ph -> D e. ( TotBnd ` B ) )
Theorem	prdsbnd2 33594*	If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- V = ( Base ` ( R ` x ) )   &    |- E = ( ( dist ` ( R ` x ) ) |` ( V X. V ) )   &    |- D = ( dist ` Y )   &    |- ( ph -> S e. W )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R Fn I )   &    |- C = ( D |` ( A X. A ) )   &    |- ( ( ph /\ x e. I ) -> E e. ( Met ` V ) )   &    |- ( ( ph /\ x e. I ) -> ( ( E |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( E |` ( y X. y ) ) e. ( Bnd ` y ) ) )   =>    |- ( ph -> ( C e. ( TotBnd ` A ) <-> C e. ( Bnd ` A ) ) )
Theorem	cntotbnd 33595	A subset of the complex numbers is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.)
|- D = ( ( abs o. - ) |` ( X X. X ) )   =>    |- ( D e. ( TotBnd ` X ) <-> D e. ( Bnd ` X ) )
Theorem	cnpwstotbnd 33596	A subset of A ^ I, where A C_ CC, is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.)
|- Y = ( (ℂfld ↾s A ) ^s I )   &    |- D = ( ( dist ` Y ) |` ( X X. X ) )   =>    |- ( ( A C_ CC /\ I e. Fin ) -> ( D e. ( TotBnd ` X ) <-> D e. ( Bnd ` X ) ) )
20.19.8  Isometries
Syntax	cismty 33597	Extend class notation with the class of metric space isometries.
class Ismty
Definition	df-ismty 33598*	Define a function which takes two metric spaces and returns the set of isometries between the spaces. An isometry is a bijection which preserves distance. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- Ismty = ( m e. U. ran *Met , n e. U. ran *Met |-> { f | ( f : dom dom m -1-1-onto-> dom dom n /\ A. x e. dom dom m A. y e. dom dom m ( x m y ) = ( ( f ` x ) n ( f ` y ) ) ) } )
Theorem	ismtyval 33599*	The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( M Ismty N ) = { f | ( f : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( f ` x ) N ( f ` y ) ) ) } )
Theorem	isismty 33600*	The condition "is an isometry". (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) <-> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) )