P. 215 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21401-21500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ptuniconst 21401	The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- J = ( Xt_ ` ( A X. { R } ) )   &    |- X = U. R   =>    |- ( ( A e. V /\ R e. Top ) -> ( X ^m A ) = U. J )
Theorem	xkouni 21402	The base set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- J = ( S ^ko R )   =>    |- ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) = U. J )
Theorem	xkotopon 21403	The base set of the compact-open topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- J = ( S ^ko R )   =>    |- ( ( R e. Top /\ S e. Top ) -> J e. (TopOn ` ( R Cn S ) ) )
Theorem	ptval2 21404*	The value of the product topology function. (Contributed by Mario Carneiro, 7-Feb-2015.)
|- J = ( Xt_ ` F )   &    |- X = U. J   &    |- G = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )   =>    |- ( ( A e. V /\ F : A --> Top ) -> J = ( topGen ` ( fi ` ( { X } u. ran G ) ) ) )
Theorem	txopn 21405	The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( ( R e. V /\ S e. W ) /\ ( A e. R /\ B e. S ) ) -> ( A X. B ) e. ( R tX S ) )
Theorem	txcld 21406	The product of two closed sets is closed in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( A X. B ) e. ( Clsd ` ( R tX S ) ) )
Theorem	txcls 21407	Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015.)
|- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( A C_ X /\ B C_ Y ) ) -> ( ( cls ` ( R tX S ) ) ` ( A X. B ) ) = ( ( ( cls ` R ) ` A ) X. ( ( cls ` S ) ` B ) ) )
Theorem	txss12 21408	Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( A tX C ) C_ ( B tX D ) )
Theorem	txbasval 21409	It is sufficient to consider products of the bases for the topologies in the topological product. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( R e. V /\ S e. W ) -> ( ( topGen ` R ) tX ( topGen ` S ) ) = ( R tX S ) )
Theorem	neitx 21410	The Cartesian product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) )
Theorem	txcnpi 21411*	Continuity of a two-argument function at a point. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) )   &    |- ( ph -> U e. L )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> ( A F B ) e. U )   =>    |- ( ph -> E. u e. J E. v e. K ( A e. u /\ B e. v /\ ( u X. v ) C_ ( `' F " U ) ) )
Theorem	tx1cn 21412	Continuity of the first projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) )
Theorem	tx2cn 21413	Continuity of the second projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) )
Theorem	ptpjcn 21414*	Continuity of a projection map into a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Feb-2015.)
|- Y = U. J   &    |- J = ( Xt_ ` F )   =>    |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. Y |-> ( x ` I ) ) e. ( J Cn ( F ` I ) ) )
Theorem	ptpjopn 21415*	The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- Y = U. J   &    |- J = ( Xt_ ` F )   =>    |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) " U ) e. ( F ` I ) )
Theorem	ptcld 21416*	A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> Top )   &    |- ( ( ph /\ k e. A ) -> C e. ( Clsd ` ( F ` k ) ) )   =>    |- ( ph -> X_ k e. A C e. ( Clsd ` ( Xt_ ` F ) ) )
Theorem	ptcldmpt 21417*	A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> J e. Top )   &    |- ( ( ph /\ k e. A ) -> C e. ( Clsd ` J ) )   =>    |- ( ph -> X_ k e. A C e. ( Clsd ` ( Xt_ ` ( k e. A |-> J ) ) ) )
Theorem	ptclsg 21418*	The closure of a box in the product topology is the box formed from the closures of the factors. The proof uses the axiom of choice; the last hypothesis is the choice assumption. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- J = ( Xt_ ` ( k e. A |-> R ) )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> R e. (TopOn ` X ) )   &    |- ( ( ph /\ k e. A ) -> S C_ X )   &    |- ( ph -> U_ k e. A S e. AC A )   =>    |- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )
Theorem	ptcls 21419*	The closure of a box in the product topology is the box formed from the closures of the factors. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( Xt_ ` ( k e. A |-> R ) )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> R e. (TopOn ` X ) )   &    |- ( ( ph /\ k e. A ) -> S C_ X )   =>    |- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )
Theorem	dfac14lem 21420*	Lemma for dfac14 21421. By equipping S u. { P } for some P e/ S with the particular point topology, we can show that P is in the closure of S; hence the sequence P ( x ) is in the product of the closures, and we can utilize this instance of ptcls 21419 to extract an element of the closure of X_ k e. I S. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ( ph -> I e. V )   &    |- ( ( ph /\ x e. I ) -> S e. W )   &    |- ( ( ph /\ x e. I ) -> S =/= (/) )   &    |- P = ~P U. S   &    |- R = { y e. ~P ( S u. { P } ) | ( P e. y -> y = ( S u. { P } ) ) }   &    |- J = ( Xt_ ` ( x e. I |-> R ) )   &    |- ( ph -> ( ( cls ` J ) ` X_ x e. I S ) = X_ x e. I ( ( cls ` R ) ` S ) )   =>    |- ( ph -> X_ x e. I S =/= (/) )
Theorem	dfac14 21421*	Theorem ptcls 21419 is an equivalent of the axiom of choice. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- (CHOICE <-> A. f ( f : dom f --> Top -> A. s e. X_ k e. dom f ~P U. ( f ` k ) ( ( cls ` ( Xt_ ` f ) ) ` X_ k e. dom f ( s ` k ) ) = X_ k e. dom f ( ( cls ` ( f ` k ) ) ` ( s ` k ) ) ) )
Theorem	xkoccn 21422*	The "constant function" function which maps x e. Y to the constant function z e. X |-> x is a continuous function from X into the space of continuous functions from Y to X. This can also be understood as the currying of the first projection function. (The currying of the second projection function is x e. Y |-> ( z e. X |-> z ), which we already know is continuous because it is a constant function.) (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( x e. Y |-> ( X X. { x } ) ) e. ( S Cn ( S ^ko R ) ) )
Theorem	txcnp 21423*	If two functions are continuous at D, then the ordered pair of them is continuous at D into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> D e. X )   &    |- ( ph -> ( x e. X |-> A ) e. ( ( J CnP K ) ` D ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( ( J CnP L ) ` D ) )   =>    |- ( ph -> ( x e. X |-> <. A , B >. ) e. ( ( J CnP ( K tX L ) ) ` D ) )
Theorem	ptcnplem 21424*	Lemma for ptcnp 21425. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- K = ( Xt_ ` F )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> Top )   &    |- ( ph -> D e. X )   &    |- ( ( ph /\ k e. I ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) )   &    |- F/ k ps   &    |- ( ( ph /\ ps ) -> G Fn I )   &    |- ( ( ( ph /\ ps ) /\ k e. I ) -> ( G ` k ) e. ( F ` k ) )   &    |- ( ( ph /\ ps ) -> W e. Fin )   &    |- ( ( ( ph /\ ps ) /\ k e. ( I \ W ) ) -> ( G ` k ) = U. ( F ` k ) )   &    |- ( ( ph /\ ps ) -> ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ k e. I ( G ` k ) )   =>    |- ( ( ph /\ ps ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( G ` k ) ) )
Theorem	ptcnp 21425*	If every projection of a function is continuous at D, then the function itself is continuous at D into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- K = ( Xt_ ` F )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> Top )   &    |- ( ph -> D e. X )   &    |- ( ( ph /\ k e. I ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) )   =>    |- ( ph -> ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` D ) )
Theorem	upxp 21426*	Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- P = ( 1st |` ( B X. C ) )   &    |- Q = ( 2nd |` ( B X. C ) )   =>    |- ( ( A e. D /\ F : A --> B /\ G : A --> C ) -> E! h ( h : A --> ( B X. C ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) )
Theorem	txcnmpt 21427*	A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- W = U. U   &    |- H = ( x e. W |-> <. ( F ` x ) , ( G ` x ) >. )   =>    |- ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> H e. ( U Cn ( R tX S ) ) )
Theorem	uptx 21428*	Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- T = ( R tX S )   &    |- X = U. R   &    |- Y = U. S   &    |- Z = ( X X. Y )   &    |- P = ( 1st |` Z )   &    |- Q = ( 2nd |` Z )   =>    |- ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> E! h e. ( U Cn T ) ( F = ( P o. h ) /\ G = ( Q o. h ) ) )
Theorem	txcn 21429	A map into the product of two topological spaces is continuous iff both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- X = U. R   &    |- Y = U. S   &    |- Z = ( X X. Y )   &    |- W = U. U   &    |- P = ( 1st |` Z )   &    |- Q = ( 2nd |` Z )   =>    |- ( ( R e. Top /\ S e. Top /\ F : W --> Z ) -> ( F e. ( U Cn ( R tX S ) ) <-> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) )
Theorem	ptcn 21430*	If every projection of a function is continuous, then the function itself is continuous into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- K = ( Xt_ ` F )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> Top )   &    |- ( ( ph /\ k e. I ) -> ( x e. X |-> A ) e. ( J Cn ( F ` k ) ) )   =>    |- ( ph -> ( x e. X |-> ( k e. I |-> A ) ) e. ( J Cn K ) )
Theorem	prdstopn 21431	Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- O = ( TopOpen ` Y )   =>    |- ( ph -> O = ( Xt_ ` ( TopOpen o. R ) ) )
Theorem	prdstps 21432	A structure product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I --> TopSp )   =>    |- ( ph -> Y e. TopSp )
Theorem	pwstps 21433	A structure product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. TopSp /\ I e. V ) -> Y e. TopSp )
Theorem	txrest 21434	The subspace of a topological product space induced by a subset with a Cartesian product representation is a topological product of the subspaces induced by the subspaces of the terms of the products. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|- ( ( ( R e. V /\ S e. W ) /\ ( A e. X /\ B e. Y ) ) -> ( ( R tX S ) ↾t ( A X. B ) ) = ( ( R ↾t A ) tX ( S ↾t B ) ) )
Theorem	txdis 21435	The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( ( A e. V /\ B e. W ) -> ( ~P A tX ~P B ) = ~P ( A X. B ) )
Theorem	txindislem 21436	Lemma for txindis 21437. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( ( _I ` A ) X. ( _I ` B ) ) = ( _I ` ( A X. B ) )
Theorem	txindis 21437	The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( { (/) , A } tX { (/) , B } ) = { (/) , ( A X. B ) }
Theorem	txdis1cn 21438*	A function is jointly continuous on a discrete left topology iff it is continuous as a function of its right argument, for each fixed left value. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- ( ph -> X e. V )   &    |- ( ph -> J e. (TopOn ` Y ) )   &    |- ( ph -> K e. Top )   &    |- ( ph -> F Fn ( X X. Y ) )   &    |- ( ( ph /\ x e. X ) -> ( y e. Y |-> ( x F y ) ) e. ( J Cn K ) )   =>    |- ( ph -> F e. ( ( ~P X tX J ) Cn K ) )
Theorem	txlly 21439*	If the property A is preserved under topological products, then so is the property of being locally A. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- ( ( j e. A /\ k e. A ) -> ( j tX k ) e. A )   =>    |- ( ( R e. Locally A /\ S e. Locally A ) -> ( R tX S ) e. Locally A )
Theorem	txnlly 21440*	If the property A is preserved under topological products, then so is the property of being n-locally A. (Contributed by Mario Carneiro, 13-Apr-2015.)
|- ( ( j e. A /\ k e. A ) -> ( j tX k ) e. A )   =>    |- ( ( R e. 𝑛Locally A /\ S e. 𝑛Locally A ) -> ( R tX S ) e. 𝑛Locally A )
Theorem	pthaus 21441	The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ( ( A e. V /\ F : A --> Haus ) -> ( Xt_ ` F ) e. Haus )
Theorem	ptrescn 21442*	Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.)
|- X = U. J   &    |- J = ( Xt_ ` F )   &    |- K = ( Xt_ ` ( F |` B ) )   =>    |- ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( x e. X |-> ( x |` B ) ) e. ( J Cn K ) )
Theorem	txtube 21443*	The "tube lemma". If X is compact and there is an open set U containing the line X X. { A }, then there is a "tube" X X. u for some neighborhood u of A which is entirely contained within U. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- X = U. R   &    |- Y = U. S   &    |- ( ph -> R e. Comp )   &    |- ( ph -> S e. Top )   &    |- ( ph -> U e. ( R tX S ) )   &    |- ( ph -> ( X X. { A } ) C_ U )   &    |- ( ph -> A e. Y )   =>    |- ( ph -> E. u e. S ( A e. u /\ ( X X. u ) C_ U ) )
Theorem	txcmplem1 21444*	Lemma for txcmp 21446. (Contributed by Mario Carneiro, 14-Sep-2014.)
|- X = U. R   &    |- Y = U. S   &    |- ( ph -> R e. Comp )   &    |- ( ph -> S e. Comp )   &    |- ( ph -> W C_ ( R tX S ) )   &    |- ( ph -> ( X X. Y ) = U. W )   &    |- ( ph -> A e. Y )   =>    |- ( ph -> E. u e. S ( A e. u /\ E. v e. ( ~P W i^i Fin ) ( X X. u ) C_ U. v ) )
Theorem	txcmplem2 21445*	Lemma for txcmp 21446. (Contributed by Mario Carneiro, 14-Sep-2014.)
|- X = U. R   &    |- Y = U. S   &    |- ( ph -> R e. Comp )   &    |- ( ph -> S e. Comp )   &    |- ( ph -> W C_ ( R tX S ) )   &    |- ( ph -> ( X X. Y ) = U. W )   =>    |- ( ph -> E. v e. ( ~P W i^i Fin ) ( X X. Y ) = U. v )
Theorem	txcmp 21446	The topological product of two compact spaces is compact. (Contributed by Mario Carneiro, 14-Sep-2014.) (Proof shortened 21-Mar-2015.)
|- ( ( R e. Comp /\ S e. Comp ) -> ( R tX S ) e. Comp )
Theorem	txcmpb 21447	The topological product of two nonempty topologies is compact iff the component topologies are both compact. (Contributed by Mario Carneiro, 14-Sep-2014.)
|- X = U. R   &    |- Y = U. S   =>    |- ( ( ( R e. Top /\ S e. Top ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( ( R tX S ) e. Comp <-> ( R e. Comp /\ S e. Comp ) ) )
Theorem	hausdiag 21448	A topology is Hausdorff iff the diagonal set is closed in the topology's product with itself. EDITORIAL: very clumsy proof, can probably be shortened substantially. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- X = U. J   =>    |- ( J e. Haus <-> ( J e. Top /\ ( _I |` X ) e. ( Clsd ` ( J tX J ) ) ) )
Theorem	hauseqlcld 21449	In a Hausdorff topology, the equalizer of two continuous functions is closed (thus, two continuous functions which agree on a dense set agree everywhere). (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> K e. Haus )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   =>    |- ( ph -> dom ( F i^i G ) e. ( Clsd ` J ) )
Theorem	txhaus 21450	The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- ( ( R e. Haus /\ S e. Haus ) -> ( R tX S ) e. Haus )
Theorem	txlm 21451*	Two sequences converge iff the sequence of their ordered pairs converges. Proposition 14-2.6 of [Gleason] p. 230. (Contributed by NM, 16-Jul-2007.) (Revised by Mario Carneiro, 5-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> F : Z --> X )   &    |- ( ph -> G : Z --> Y )   &    |- H = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. )   =>    |- ( ph -> ( ( F ( ~~> t ` J ) R /\ G ( ~~> t ` K ) S ) <-> H ( ~~> t ` ( J tX K ) ) <. R , S >. ) )
Theorem	lmcn2 21452*	The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 15-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> F : Z --> X )   &    |- ( ph -> G : Z --> Y )   &    |- ( ph -> F ( ~~> t ` J ) R )   &    |- ( ph -> G ( ~~> t ` K ) S )   &    |- ( ph -> O e. ( ( J tX K ) Cn N ) )   &    |- H = ( n e. Z |-> ( ( F ` n ) O ( G ` n ) ) )   =>    |- ( ph -> H ( ~~> t ` N ) ( R O S ) )
Theorem	tx1stc 21453	The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( R e. 1stc /\ S e. 1stc ) -> ( R tX S ) e. 1stc )
Theorem	tx2ndc 21454	The topological product of two second-countable spaces is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( R e. 2ndc /\ S e. 2ndc ) -> ( R tX S ) e. 2ndc )
Theorem	txkgen 21455	The topological product of a locally compact space and a compactly generated Hausdorff space is compactly generated. (The condition on S can also be replaced with either "compactly generated weak Hausdorff (CGWH)" or "compact Hausdorff-ly generated (CHG)", where WH means that all images of compact Hausdorff spaces are closed and CHG means that a set is open iff it is open in all compact Hausdorff spaces.) (Contributed by Mario Carneiro, 23-Mar-2015.)
|- ( ( R e. 𝑛Locally Comp /\ S e. ( ran 𝑘Gen i^i Haus ) ) -> ( R tX S ) e. ran 𝑘Gen )
Theorem	xkohaus 21456	If the codomain space is Hausdorff, then the compact-open topology of continuous functions is also Hausdorff. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( R e. Top /\ S e. Haus ) -> ( S ^ko R ) e. Haus )
Theorem	xkoptsub 21457	The compact-open topology is finer than the product topology restricted to continuous functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- X = U. R   &    |- J = ( Xt_ ` ( X X. { S } ) )   =>    |- ( ( R e. Top /\ S e. Top ) -> ( J ↾t ( R Cn S ) ) C_ ( S ^ko R ) )
Theorem	xkopt 21458	The compact-open topology on a discrete set coincides with the product topology where all the factors are the same. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- ( ( R e. Top /\ A e. V ) -> ( R ^ko ~P A ) = ( Xt_ ` ( A X. { R } ) ) )
Theorem	xkopjcn 21459*	Continuity of a projection map from the space of continuous functions. (This theorem can be strengthened, to joint continuity in both f and A as a function on ( S ^ko R ) tX R, but not without stronger assumptions on R; see xkofvcn 21487.) (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- X = U. R   =>    |- ( ( R e. Top /\ S e. Top /\ A e. X ) -> ( f e. ( R Cn S ) |-> ( f ` A ) ) e. ( ( S ^ko R ) Cn S ) )
Theorem	xkoco1cn 21460*	If F is a continuous function, then g |-> g o. F is a continuous function on function spaces. (The reason we prove this and xkoco2cn 21461 independently of the more general xkococn 21463 is because that requires some inconvenient extra assumptions on S.) (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( ph -> T e. Top )   &    |- ( ph -> F e. ( R Cn S ) )   =>    |- ( ph -> ( g e. ( S Cn T ) |-> ( g o. F ) ) e. ( ( T ^ko S ) Cn ( T ^ko R ) ) )
Theorem	xkoco2cn 21461*	If F is a continuous function, then g |-> F o. g is a continuous function on function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- ( ph -> R e. Top )   &    |- ( ph -> F e. ( S Cn T ) )   =>    |- ( ph -> ( g e. ( R Cn S ) |-> ( F o. g ) ) e. ( ( S ^ko R ) Cn ( T ^ko R ) ) )
Theorem	xkococnlem 21462*	Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- F = ( f e. ( S Cn T ) , g e. ( R Cn S ) |-> ( f o. g ) )   &    |- ( ph -> S e. 𝑛Locally Comp )   &    |- ( ph -> K C_ U. R )   &    |- ( ph -> ( R ↾t K ) e. Comp )   &    |- ( ph -> V e. T )   &    |- ( ph -> A e. ( S Cn T ) )   &    |- ( ph -> B e. ( R Cn S ) )   &    |- ( ph -> ( ( A o. B ) " K ) C_ V )   =>    |- ( ph -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
Theorem	xkococn 21463*	Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- F = ( f e. ( S Cn T ) , g e. ( R Cn S ) |-> ( f o. g ) )   =>    |- ( ( R e. Top /\ S e. 𝑛Locally Comp /\ T e. Top ) -> F e. ( ( ( T ^ko S ) tX ( S ^ko R ) ) Cn ( T ^ko R ) ) )
12.1.19  Continuous function-builders
Theorem	cnmptid 21464*	The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   =>    |- ( ph -> ( x e. X |-> x ) e. ( J Cn J ) )
Theorem	cnmptc 21465*	A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> P e. Y )   =>    |- ( ph -> ( x e. X |-> P ) e. ( J Cn K ) )
Theorem	cnmpt11 21466*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( y e. Y |-> B ) e. ( K Cn L ) )   &    |- ( y = A -> B = C )   =>    |- ( ph -> ( x e. X |-> C ) e. ( J Cn L ) )
Theorem	cnmpt11f 21467*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> F e. ( K Cn L ) )   =>    |- ( ph -> ( x e. X |-> ( F ` A ) ) e. ( J Cn L ) )
Theorem	cnmpt1t 21468*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( J Cn L ) )   =>    |- ( ph -> ( x e. X |-> <. A , B >. ) e. ( J Cn ( K tX L ) ) )
Theorem	cnmpt12f 21469*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( J Cn L ) )   &    |- ( ph -> F e. ( ( K tX L ) Cn M ) )   =>    |- ( ph -> ( x e. X |-> ( A F B ) ) e. ( J Cn M ) )
Theorem	cnmpt12 21470*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( J Cn L ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> ( y e. Y , z e. Z |-> C ) e. ( ( K tX L ) Cn M ) )   &    |- ( ( y = A /\ z = B ) -> C = D )   =>    |- ( ph -> ( x e. X |-> D ) e. ( J Cn M ) )
Theorem	cnmpt1st 21471*	The projection onto the first coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )
Theorem	cnmpt2nd 21472*	The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )
Theorem	cnmpt2c 21473*	A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> P e. Z )   =>    |- ( ph -> ( x e. X , y e. Y |-> P ) e. ( ( J tX K ) Cn L ) )
Theorem	cnmpt21 21474*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) )   &    |- ( z = A -> B = C )   =>    |- ( ph -> ( x e. X , y e. Y |-> C ) e. ( ( J tX K ) Cn M ) )
Theorem	cnmpt21f 21475*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> F e. ( L Cn M ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> ( F ` A ) ) e. ( ( J tX K ) Cn M ) )
Theorem	cnmpt2t 21476*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> <. A , B >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
Theorem	cnmpt22 21477*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> M e. (TopOn ` W ) )   &    |- ( ph -> ( z e. Z , w e. W |-> C ) e. ( ( L tX M ) Cn N ) )   &    |- ( ( z = A /\ w = B ) -> C = D )   =>    |- ( ph -> ( x e. X , y e. Y |-> D ) e. ( ( J tX K ) Cn N ) )
Theorem	cnmpt22f 21478*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )   &    |- ( ph -> F e. ( ( L tX M ) Cn N ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> ( A F B ) ) e. ( ( J tX K ) Cn N ) )
Theorem	cnmpt1res 21479*	The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.)
|- K = ( J ↾t Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn L ) )   =>    |- ( ph -> ( x e. Y |-> A ) e. ( K Cn L ) )
Theorem	cnmpt2res 21480*	The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- K = ( J ↾t Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y C_ X )   &    |- N = ( M ↾t W )   &    |- ( ph -> M e. (TopOn ` Z ) )   &    |- ( ph -> W C_ Z )   &    |- ( ph -> ( x e. X , y e. Z |-> A ) e. ( ( J tX M ) Cn L ) )   =>    |- ( ph -> ( x e. Y , y e. W |-> A ) e. ( ( K tX N ) Cn L ) )
Theorem	cnmptcom 21481*	The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   =>    |- ( ph -> ( y e. Y , x e. X |-> A ) e. ( ( K tX J ) Cn L ) )
Theorem	cnmptkc 21482*	The curried first projection function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   =>    |- ( ph -> ( x e. X |-> ( y e. Y |-> x ) ) e. ( J Cn ( J ^ko K ) ) )
Theorem	cnmptkp 21483*	The evaluation of the inner function in a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )   &    |- ( ph -> B e. Y )   &    |- ( y = B -> A = C )   =>    |- ( ph -> ( x e. X |-> C ) e. ( J Cn L ) )
Theorem	cnmptk1 21484*	The composition of a curried function with a one-arg function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )   &    |- ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) )   &    |- ( z = A -> B = C )   =>    |- ( ph -> ( x e. X |-> ( y e. Y |-> C ) ) e. ( J Cn ( M ^ko K ) ) )
Theorem	cnmpt1k 21485*	The composition of a one-arg function with a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> M e. (TopOn ` W ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn L ) )   &    |- ( ph -> ( y e. Y |-> ( z e. Z |-> B ) ) e. ( K Cn ( M ^ko L ) ) )   &    |- ( z = A -> B = C )   =>    |- ( ph -> ( y e. Y |-> ( x e. X |-> C ) ) e. ( K Cn ( M ^ko J ) ) )
Theorem	cnmptkk 21486*	The composition of two curried functions is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> M e. (TopOn ` W ) )   &    |- ( ph -> L e. 𝑛Locally Comp )   &    |- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )   &    |- ( ph -> ( x e. X |-> ( z e. Z |-> B ) ) e. ( J Cn ( M ^ko L ) ) )   &    |- ( z = A -> B = C )   =>    |- ( ph -> ( x e. X |-> ( y e. Y |-> C ) ) e. ( J Cn ( M ^ko K ) ) )
Theorem	xkofvcn 21487*	Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn 21459.) (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- X = U. R   &    |- F = ( f e. ( R Cn S ) , x e. X |-> ( f ` x ) )   =>    |- ( ( R e. 𝑛Locally Comp /\ S e. Top ) -> F e. ( ( ( S ^ko R ) tX R ) Cn S ) )
Theorem	cnmptk1p 21488*	The evaluation of a curried function by a one-arg function is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> K e. 𝑛Locally Comp )   &    |- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( J Cn K ) )   &    |- ( y = B -> A = C )   =>    |- ( ph -> ( x e. X |-> C ) e. ( J Cn L ) )
Theorem	cnmptk2 21489*	The uncurrying of a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> K e. 𝑛Locally Comp )   &    |- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
Theorem	xkoinjcn 21490*	Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- F = ( x e. X |-> ( y e. Y |-> <. y , x >. ) )   =>    |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> F e. ( R Cn ( ( S tX R ) ^ko S ) ) )
Theorem	cnmpt2k 21491*	The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   =>    |- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
Theorem	txconn 21492	The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.)
|- ( ( R e. Conn /\ S e. Conn ) -> ( R tX S ) e. Conn )
Theorem	imasnopn 21493	If a relation graph is open, then an image set of a singleton is also open. Corollary of proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( J tX K ) /\ A e. X ) ) -> ( R " { A } ) e. K )
Theorem	imasncld 21494	If a relation graph is closed, then an image set of a singleton is also closed. Corollary of proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( Clsd ` ( J tX K ) ) /\ A e. X ) ) -> ( R " { A } ) e. ( Clsd ` K ) )
Theorem	imasncls 21495	If a relation graph is closed, then an image set of a singleton is also closed. Corollary of proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( R C_ ( X X. Y ) /\ A e. X ) ) -> ( ( cls ` K ) ` ( R " { A } ) ) C_ ( ( ( cls ` ( J tX K ) ) ` R ) " { A } ) )
12.1.20  Quotient maps and quotient topology
Syntax	ckq 21496	Extend class notation with the Kolmogorov quotient function.
class KQ
Definition	df-kq 21497*	Define the Kolmogorov quotient. This is a function on topologies which maps a topology to its quotient under the topological distinguishability map, which takes a point to the set of open sets that contain it. Two points are mapped to the same image under this function iff they are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- KQ = ( j e. Top |-> ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) )
Theorem	qtopval 21498*	Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. V /\ F e. W ) -> ( J qTop F ) = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )
Theorem	qtopval2 21499*	Value of the quotient topology function when F is a function on the base set. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( J qTop F ) = { s e. ~P Y | ( `' F " s ) e. J } )
Theorem	elqtop 21500	Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )