P. 202 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20101-20200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ptcnp 20101*	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 20102*	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 20103*	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 20104*	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 20105	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 20106*	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 20107	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 20108	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 20109	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 20110	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 20111	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 20112	Lemma for txindis 20113. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( ( _I ` A ) X. ( _I ` B ) ) = ( _I ` ( A X. B ) )
Theorem	txindis 20113	The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( { (/) , A } tX { (/) , B } ) = { (/) , ( A X. B ) }
Theorem	txdis1cn 20114*	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 20115*	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 20116*	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 20117	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 20118*	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 20119*	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 20120*	Lemma for txcmp 20122. (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 20121*	Lemma for txcmp 20122. (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 20122	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 20123	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 20124	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 20125	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 20126	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 20127*	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 20128*	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 20129	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 20130	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 20131	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 20132	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 20133	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 20134	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 20135*	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 20163.) (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 20136*	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 20137 independently of the more general xkococn 20139 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 20137*	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 20138*	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 20139*	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 20140*	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 20141*	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 20142*	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 20143*	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 20144*	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 20145*	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 20146*	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 20147*	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 20148*	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 20149*	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 20150*	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 20151*	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 20152*	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 20153*	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 20154*	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 20155*	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 20156*	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 20157*	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 20158*	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 20159*	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 20160*	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 20161*	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 20162*	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 20163*	Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn 20135.) (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 20164*	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 20165*	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 20166*	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 20167*	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	txcon 20168	The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.)
|- ( ( R e. Con /\ S e. Con ) -> ( R tX S ) e. Con )
Theorem	imasnopn 20169	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 20170	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 20171	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 20172	Extend class notation with the Kolmogorov quotient function.
class KQ
Definition	df-kq 20173*	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 20174*	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 20175*	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 20176	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 ) ) )
Theorem	qtopres 20177	The quotient topology is unaffected by restriction to the base set. This property makes it slightly more convenient to use, since we don't have to require that F be a function with domain X. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- X = U. J   =>    |- ( F e. V -> ( J qTop F ) = ( J qTop ( F |` X ) ) )
Theorem	qtoptop2 20178	The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- ( ( J e. Top /\ F e. V /\ Fun F ) -> ( J qTop F ) e. Top )
Theorem	qtoptop 20179	The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ F Fn X ) -> ( J qTop F ) e. Top )
Theorem	elqtop2 20180	Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.)
|- X = U. J   =>    |- ( ( J e. V /\ F : X -onto-> Y ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )
Theorem	qtopuni 20181	The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ F : X -onto-> Y ) -> Y = U. ( J qTop F ) )
Theorem	elqtop3 20182	Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.)
|- ( ( J e. (TopOn ` X ) /\ F : X -onto-> Y ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )
Theorem	qtoptopon 20183	The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. (TopOn ` Y ) )
Theorem	qtopid 20184	A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- ( ( J e. (TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
Theorem	idqtop 20185	The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( J e. (TopOn ` X ) -> ( J qTop ( _I |` X ) ) = J )
Theorem	qtopcmplem 20186	Lemma for qtopcmp 20187 and qtopcon 20188. (Contributed by Mario Carneiro, 24-Mar-2015.)
|- X = U. J   &    |- ( J e. A -> J e. Top )   &    |- ( ( J e. A /\ F : X -onto-> U. ( J qTop F ) /\ F e. ( J Cn ( J qTop F ) ) ) -> ( J qTop F ) e. A )   =>    |- ( ( J e. A /\ F Fn X ) -> ( J qTop F ) e. A )
Theorem	qtopcmp 20187	A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Comp /\ F Fn X ) -> ( J qTop F ) e. Comp )
Theorem	qtopcon 20188	A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Con /\ F Fn X ) -> ( J qTop F ) e. Con )
Theorem	qtopkgen 20189	A quotient of a compactly generated space is compactly generated. (Contributed by Mario Carneiro, 9-Apr-2015.)
|- X = U. J   =>    |- ( ( J e. ran 𝑘Gen /\ F Fn X ) -> ( J qTop F ) e. ran 𝑘Gen )
Theorem	basqtop 20190	An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( J qTop F ) e. TopBases )
Theorem	tgqtop 20191	An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( topGen ` J ) qTop F ) = ( topGen ` ( J qTop F ) ) )
Theorem	qtopcld 20192	The property of being a closed set in the quotient topology. (Contributed by Mario Carneiro, 24-Mar-2015.)
|- ( ( J e. (TopOn ` X ) /\ F : X -onto-> Y ) -> ( A e. ( Clsd ` ( J qTop F ) ) <-> ( A C_ Y /\ ( `' F " A ) e. ( Clsd ` J ) ) ) )
Theorem	qtopcn 20193	Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( G e. ( ( J qTop F ) Cn K ) <-> ( G o. F ) e. ( J Cn K ) ) )
Theorem	qtopss 20194	A surjective continuous function from J to K induces a topology J qTop F on the base set of K. This topology is in general finer than K. Together with qtopid 20184, this implies that J qTop F is the finest topology making F continuous, i.e. the final topology with respect to the family { F }. (Contributed by Mario Carneiro, 24-Mar-2015.)
|- ( ( F e. ( J Cn K ) /\ K e. (TopOn ` Y ) /\ ran F = Y ) -> K C_ ( J qTop F ) )
Theorem	qtopeu 20195*	Universal property of the quotient topology. If G is a function from J to K which is equal on all equivalent elements under F, then there is a unique continuous map f : ( J / F ) --> K such that G = f o. F, and we say that G "passes to the quotient". (Contributed by Mario Carneiro, 24-Mar-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> G e. ( J Cn K ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) ) -> ( G ` x ) = ( G ` y ) )   =>    |- ( ph -> E! f e. ( ( J qTop F ) Cn K ) G = ( f o. F ) )
Theorem	qtoprest 20196	If A is a saturated open or closed set (where saturated means that A = ( `' F " U ) for some U), then the restriction of the quotient map F to A is a quotient map. (Contributed by Mario Carneiro, 24-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F : X -onto-> Y )   &    |- ( ph -> U C_ Y )   &    |- ( ph -> A = ( `' F " U ) )   &    |- ( ph -> ( A e. J \/ A e. ( Clsd ` J ) ) )   =>    |- ( ph -> ( ( J qTop F ) ↾t U ) = ( ( J ↾t A ) qTop ( F |` A ) ) )
Theorem	qtopomap 20197*	If F is a surjective continuous open map, then it is a quotient map. (An open map is a function that maps open sets to open sets.) (Contributed by Mario Carneiro, 24-Mar-2015.)
|- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> ran F = Y )   &    |- ( ( ph /\ x e. J ) -> ( F " x ) e. K )   =>    |- ( ph -> K = ( J qTop F ) )
Theorem	qtopcmap 20198*	If F is a surjective continuous closed map, then it is a quotient map. (A closed map is a function that maps closed sets to closed sets.) (Contributed by Mario Carneiro, 24-Mar-2015.)
|- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> ran F = Y )   &    |- ( ( ph /\ x e. ( Clsd ` J ) ) -> ( F " x ) e. ( Clsd ` K ) )   =>    |- ( ph -> K = ( J qTop F ) )
Theorem	imastopn 20199	The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. W )   &    |- J = ( TopOpen ` R )   &    |- O = ( TopOpen ` U )   =>    |- ( ph -> O = ( J qTop F ) )
Theorem	imastps 20200	The image of a topological space under a function is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. TopSp )   =>    |- ( ph -> U e. TopSp )