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	refun0 20101	Adding the empty set preserves refinements. (Contributed by Thierry Arnoux, 31-Jan-2020.)
|- ( ( A Ref B /\ B =/= (/) ) -> ( A u. { (/) } ) Ref B )
Theorem	isptfin 20102*	The statement "is a point-finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.)
|- X = U. A   =>    |- ( A e. B -> ( A e. PtFin <-> A. x e. X { y e. A | x e. y } e. Fin ) )
Theorem	islocfin 20103*	The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.)
|- X = U. J   &    |- Y = U. A   =>    |- ( A e. ( LocFin ` J ) <-> ( J e. Top /\ X = Y /\ A. x e. X E. n e. J ( x e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) ) )
Theorem	finptfin 20104	A finite cover is a point-finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.)
|- ( A e. Fin -> A e. PtFin )
Theorem	ptfinfin 20105*	A point covered by a point-finite cover is only covered by finitely many elements. (Contributed by Jeff Hankins, 21-Jan-2010.)
|- X = U. A   =>    |- ( ( A e. PtFin /\ P e. X ) -> { x e. A | P e. x } e. Fin )
Theorem	finlocfin 20106	A finite cover of a topological space is a locally finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.)
|- X = U. J   &    |- Y = U. A   =>    |- ( ( J e. Top /\ A e. Fin /\ X = Y ) -> A e. ( LocFin ` J ) )
Theorem	locfintop 20107	A locally finite cover covers a topological space. (Contributed by Jeff Hankins, 21-Jan-2010.)
|- ( A e. ( LocFin ` J ) -> J e. Top )
Theorem	locfinbas 20108	A locally finite cover must cover the base set of its corresponding topological space. (Contributed by Jeff Hankins, 21-Jan-2010.)
|- X = U. J   &    |- Y = U. A   =>    |- ( A e. ( LocFin ` J ) -> X = Y )
Theorem	locfinnei 20109*	A point covered by a locally finite cover has a neighborhood which intersects only finitely many elements of the cover. (Contributed by Jeff Hankins, 21-Jan-2010.)
|- X = U. J   =>    |- ( ( A e. ( LocFin ` J ) /\ P e. X ) -> E. n e. J ( P e. n /\ { s e. A | ( s i^i n ) =/= (/) } e. Fin ) )
Theorem	lfinpfin 20110	A locally finite cover is point-finite. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
|- ( A e. ( LocFin ` J ) -> A e. PtFin )
Theorem	lfinun 20111	Adding a finite set preserves locally finite covers. (Contributed by Thierry Arnoux, 31-Jan-2020.)
|- ( ( A e. ( LocFin ` J ) /\ B e. Fin /\ U. B C_ U. J ) -> ( A u. B ) e. ( LocFin ` J ) )
Theorem	locfincmp 20112	For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
|- X = U. J   &    |- Y = U. C   =>    |- ( J e. Comp -> ( C e. ( LocFin ` J ) <-> ( C e. Fin /\ X = Y ) ) )
Theorem	unisngl 20113*	Taking the union of the set of singletons recovers the initial set. (Contributed by Thierry Arnoux, 9-Jan-2020.)
|- C = { u | E. x e. X u = { x } }   =>    |- X = U. C
Theorem	dissnref 20114*	The set of singletons is a refinement of any open covering of the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.)
|- C = { u | E. x e. X u = { x } }   =>    |- ( ( X e. V /\ U. Y = X ) -> C Ref Y )
Theorem	dissnlocfin 20115*	The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.)
|- C = { u | E. x e. X u = { x } }   =>    |- ( X e. V -> C e. ( LocFin ` ~P X ) )
Theorem	locfindis 20116	The locally finite covers of a discrete space are precisely the point-finite covers. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
|- Y = U. C   =>    |- ( C e. ( LocFin ` ~P X ) <-> ( C e. PtFin /\ X = Y ) )
Theorem	locfincf 20117	A locally finite cover in a coarser topology is locally finite in a finer topology. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
|- X = U. J   =>    |- ( ( K e. (TopOn ` X ) /\ J C_ K ) -> ( LocFin ` J ) C_ ( LocFin ` K ) )
Theorem	comppfsc 20118*	A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
|- X = U. J   =>    |- ( J e. Top -> ( J e. Comp <-> A. c e. ~P J ( X = U. c -> E. d e. PtFin ( d C_ c /\ X = U. d ) ) ) )
12.1.17  Compactly generated spaces
Syntax	ckgen 20119	Extend class notation with the compact generator operation.
class 𝑘Gen
Definition	df-kgen 20120*	Define the "compact generator", the functor from topological spaces to compactly generated spaces. Also known as the k-ification operation. A set is k-open, i.e. x e. (𝑘Gen ` j ), iff the preimage of x is open in all compact Hausdorff spaces. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- 𝑘Gen = ( j e. Top |-> { x e. ~P U. j | A. k e. ~P U. j ( ( j ↾t k ) e. Comp -> ( x i^i k ) e. ( j ↾t k ) ) } )
Theorem	kgenval 20121*	Value of the compact generator. (The "k" in 𝑘Gen comes from the name "k-space" for these spaces, after the German word kompakt.) (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( J e. (TopOn ` X ) -> (𝑘Gen ` J ) = { x e. ~P X | A. k e. ~P X ( ( J ↾t k ) e. Comp -> ( x i^i k ) e. ( J ↾t k ) ) } )
Theorem	elkgen 20122*	Value of the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( J e. (TopOn ` X ) -> ( A e. (𝑘Gen ` J ) <-> ( A C_ X /\ A. k e. ~P X ( ( J ↾t k ) e. Comp -> ( A i^i k ) e. ( J ↾t k ) ) ) ) )
Theorem	kgeni 20123	Property of the open sets in the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( ( A e. (𝑘Gen ` J ) /\ ( J ↾t K ) e. Comp ) -> ( A i^i K ) e. ( J ↾t K ) )
Theorem	kgentopon 20124	The compact generator generates a topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( J e. (TopOn ` X ) -> (𝑘Gen ` J ) e. (TopOn ` X ) )
Theorem	kgenuni 20125	The base set of the compact generator is the same as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- X = U. J   =>    |- ( J e. Top -> X = U. (𝑘Gen ` J ) )
Theorem	kgenftop 20126	The compact generator generates a topology. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( J e. Top -> (𝑘Gen ` J ) e. Top )
Theorem	kgenf 20127	The compact generator is a function on topologies. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- 𝑘Gen : Top --> Top
Theorem	kgentop 20128	A compactly generated space is a topology. (Note: henceforth we will use the idiom " J e. ran 𝑘Gen " to denote " J is compactly generated", since as we will show a space is compactly generated iff it is in the range of the compact generator.) (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( J e. ran 𝑘Gen -> J e. Top )
Theorem	kgenss 20129	The compact generator generates a finer topology than the original. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( J e. Top -> J C_ (𝑘Gen ` J ) )
Theorem	kgenhaus 20130	The compact generator generates another Hausdorff topology given a Hausdorff topology to start from. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( J e. Haus -> (𝑘Gen ` J ) e. Haus )
Theorem	kgencmp 20131	The compact generator topology is the same as the original topology on compact subspaces. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( ( J e. Top /\ ( J ↾t K ) e. Comp ) -> ( J ↾t K ) = ( (𝑘Gen ` J ) ↾t K ) )
Theorem	kgencmp2 20132	The compact generator topology has the same compact sets as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( J e. Top -> ( ( J ↾t K ) e. Comp <-> ( (𝑘Gen ` J ) ↾t K ) e. Comp ) )
Theorem	kgenidm 20133	The compact generator is idempotent on compactly generated spaces. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( J e. ran 𝑘Gen -> (𝑘Gen ` J ) = J )
Theorem	iskgen2 20134	A space is compactly generated iff it contains its image under the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- ( J e. ran 𝑘Gen <-> ( J e. Top /\ (𝑘Gen ` J ) C_ J ) )
Theorem	iskgen3 20135*	Derive the usual definition of "compactly generated". A topology is compactly generated if every subset of X that is open in every compact subset is open. (Contributed by Mario Carneiro, 20-Mar-2015.)
|- X = U. J   =>    |- ( J e. ran 𝑘Gen <-> ( J e. Top /\ A. x e. ~P X ( A. k e. ~P X ( ( J ↾t k ) e. Comp -> ( x i^i k ) e. ( J ↾t k ) ) -> x e. J ) ) )
Theorem	llycmpkgen2 20136*	A locally compact space is compactly generated. (This variant of llycmpkgen 20138 uses the weaker definition of locally compact, "every point has a compact neighborhood", instead of "every point has a local base of compact neighborhoods".) (Contributed by Mario Carneiro, 21-Mar-2015.)
|- X = U. J   &    |- ( ph -> J e. Top )   &    |- ( ( ph /\ x e. X ) -> E. k e. ( ( nei ` J ) ` { x } ) ( J ↾t k ) e. Comp )   =>    |- ( ph -> J e. ran 𝑘Gen )
Theorem	cmpkgen 20137	A compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( J e. Comp -> J e. ran 𝑘Gen )
Theorem	llycmpkgen 20138	A locally compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( J e. 𝑛Locally Comp -> J e. ran 𝑘Gen )
Theorem	1stckgenlem 20139	The one-point compactification of NN is compact. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F : NN --> X )   &    |- ( ph -> F ( ~~> t ` J ) A )   =>    |- ( ph -> ( J ↾t ( ran F u. { A } ) ) e. Comp )
Theorem	1stckgen 20140	A first-countable space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( J e. 1stc -> J e. ran 𝑘Gen )
Theorem	kgen2ss 20141	The compact generator preserves the subset (fineness) relationship on topologies. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) /\ J C_ K ) -> (𝑘Gen ` J ) C_ (𝑘Gen ` K ) )
Theorem	kgencn 20142*	A function from a compactly generated space is continuous iff it is continuous "on compacta". (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( (𝑘Gen ` J ) Cn K ) <-> ( F : X --> Y /\ A. k e. ~P X ( ( J ↾t k ) e. Comp -> ( F |` k ) e. ( ( J ↾t k ) Cn K ) ) ) ) )
Theorem	kgencn2 20143*	A function F : J --> K from a compactly generated space is continuous iff for all compact spaces z and continuous g : z --> J, the composite F o. g : z --> K is continuous. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( (𝑘Gen ` J ) Cn K ) <-> ( F : X --> Y /\ A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) ) ) )
Theorem	kgencn3 20144	The set of continuous functions from J to K is unaffected by k-ification of K, if J is already compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( J e. ran 𝑘Gen /\ K e. Top ) -> ( J Cn K ) = ( J Cn (𝑘Gen ` K ) ) )
Theorem	kgen2cn 20145	A continuous function is also continuous with the domain and codomain replaced by their compact generator topologies. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( F e. ( J Cn K ) -> F e. ( (𝑘Gen ` J ) Cn (𝑘Gen ` K ) ) )
12.1.18  Product topologies
Syntax	ctx 20146	Extend class notation with the binary topological product operation.
class tX
Syntax	cxko 20147	Extend class notation with a function whose value is the compact-open topology.
class ^ko
Definition	df-tx 20148*	Define the binary topological product, which is homeomorphic to the general topological product over a two element set, but is more convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
Definition	df-xko 20149*	Define the compact-open topology, which is the natural topology on the set of continuous functions between two topological spaces. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ^ko = ( s e. Top , r e. Top |-> ( topGen ` ( fi ` ran ( k e. { x e. ~P U. r | ( r ↾t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } ) ) ) )
Theorem	txval 20150*	Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   =>    |- ( ( R e. V /\ S e. W ) -> ( R tX S ) = ( topGen ` B ) )
Theorem	txuni2 20151*	The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   &    |- X = U. R   &    |- Y = U. S   =>    |- ( X X. Y ) = U. B
Theorem	txbasex 20152*	The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   =>    |- ( ( R e. V /\ S e. W ) -> B e. _V )
Theorem	txbas 20153*	The set of Cartesian products of elements from two topological bases is a basis. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   =>    |- ( ( R e. TopBases /\ S e. TopBases ) -> B e. TopBases )
Theorem	eltx 20154*	A set in a product is open iff each point is surrounded by an open rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( ( J e. V /\ K e. W ) -> ( S e. ( J tX K ) <-> A. p e. S E. x e. J E. y e. K ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) ) )
Theorem	txtop 20155	The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
Theorem	ptval 20156*	The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   =>    |- ( ( A e. V /\ F Fn A ) -> ( Xt_ ` F ) = ( topGen ` B ) )
Theorem	ptpjpre1 20157*	The preimage of a projection function can be expressed as an indexed cartesian product. (Contributed by Mario Carneiro, 6-Feb-2015.)
|- X = X_ k e. A U. ( F ` k )   =>    |- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( `' ( w e. X |-> ( w ` I ) ) " U ) = X_ k e. A if ( k = I , U , U. ( F ` k ) ) )
Theorem	elpt 20158*	Elementhood in the bases of a product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   =>    |- ( S e. B <-> E. h ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. w e. Fin A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) ) /\ S = X_ y e. A ( h ` y ) ) )
Theorem	elptr 20159*	A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   =>    |- ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) ) -> X_ y e. A ( G ` y ) e. B )
Theorem	elptr2 20160*	A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   &    |- ( ph -> A e. V )   &    |- ( ph -> W e. Fin )   &    |- ( ( ph /\ k e. A ) -> S e. ( F ` k ) )   &    |- ( ( ph /\ k e. ( A \ W ) ) -> S = U. ( F ` k ) )   =>    |- ( ph -> X_ k e. A S e. B )
Theorem	ptbasid 20161*	The base set of the product topology is a basic open set. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   =>    |- ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) e. B )
Theorem	ptuni2 20162*	The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   =>    |- ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. B )
Theorem	ptbasin 20163*	The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   =>    |- ( ( ( A e. V /\ F : A --> Top ) /\ ( X e. B /\ Y e. B ) ) -> ( X i^i Y ) e. B )
Theorem	ptbasin2 20164*	The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   =>    |- ( ( A e. V /\ F : A --> Top ) -> ( fi ` B ) = B )
Theorem	ptbas 20165*	The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   =>    |- ( ( A e. V /\ F : A --> Top ) -> B e. TopBases )
Theorem	ptpjpre2 20166*	The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   &    |- X = X_ n e. A U. ( F ` n )   =>    |- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( `' ( w e. X |-> ( w ` I ) ) " U ) e. B )
Theorem	ptbasfi 20167*	The basis for the product topology can also be written as the set of finite intersections of "cylinder sets", the preimages of projections into one factor from open sets in the factor. (We have to add X itself to the list because if A is empty we get ( fi ` (/) ) = (/) while B = { (/) }.) (Contributed by Mario Carneiro, 3-Feb-2015.)
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }   &    |- X = X_ n e. A U. ( F ` n )   =>    |- ( ( A e. V /\ F : A --> Top ) -> B = ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
Theorem	pttop 20168	The product topology is a topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) e. Top )
Theorem	ptopn 20169*	A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> Top )   &    |- ( ph -> W e. Fin )   &    |- ( ( ph /\ k e. A ) -> S e. ( F ` k ) )   &    |- ( ( ph /\ k e. ( A \ W ) ) -> S = U. ( F ` k ) )   =>    |- ( ph -> X_ k e. A S e. ( Xt_ ` F ) )
Theorem	ptopn2 20170*	A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> Top )   &    |- ( ph -> O e. ( F ` Y ) )   =>    |- ( ph -> X_ k e. A if ( k = Y , O , U. ( F ` k ) ) e. ( Xt_ ` F ) )
Theorem	xkotf 20171*	Functionality of function T. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- X = U. R   &    |- K = { x e. ~P X | ( R ↾t x ) e. Comp }   &    |- T = ( k e. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } )   =>    |- T : ( K X. S ) --> ~P ( R Cn S )
Theorem	xkobval 20172*	Alternative expression for the subbase of the compact-open topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- X = U. R   &    |- K = { x e. ~P X | ( R ↾t x ) e. Comp }   &    |- T = ( k e. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } )   =>    |- ran T = { s | E. k e. ~P X E. v e. S ( ( R ↾t k ) e. Comp /\ s = { f e. ( R Cn S ) | ( f " k ) C_ v } ) }
Theorem	xkoval 20173*	Value of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- X = U. R   &    |- K = { x e. ~P X | ( R ↾t x ) e. Comp }   &    |- T = ( k e. K , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } )   =>    |- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) = ( topGen ` ( fi ` ran T ) ) )
Theorem	xkotop 20174	The compact-open topology is a topology. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top )
Theorem	xkoopn 20175*	A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- X = U. R   &    |- ( ph -> R e. Top )   &    |- ( ph -> S e. Top )   &    |- ( ph -> A C_ X )   &    |- ( ph -> ( R ↾t A ) e. Comp )   &    |- ( ph -> U e. S )   =>    |- ( ph -> { f e. ( R Cn S ) | ( f " A ) C_ U } e. ( S ^ko R ) )
Theorem	txtopi 20176	The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- R e. Top   &    |- S e. Top   =>    |- ( R tX S ) e. Top
Theorem	txtopon 20177	The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro, 2-Sep-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( R tX S ) e. (TopOn ` ( X X. Y ) ) )
Theorem	txuni 20178	The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- X = U. R   &    |- Y = U. S   =>    |- ( ( R e. Top /\ S e. Top ) -> ( X X. Y ) = U. ( R tX S ) )
Theorem	txunii 20179	The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- R e. Top   &    |- S e. Top   &    |- X = U. R   &    |- Y = U. S   =>    |- ( X X. Y ) = U. ( R tX S )
Theorem	ptuni 20180*	The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- J = ( Xt_ ` F )   =>    |- ( ( A e. V /\ F : A --> Top ) -> X_ x e. A U. ( F ` x ) = U. J )
Theorem	ptunimpt 20181*	Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- J = ( Xt_ ` ( x e. A |-> K ) )   =>    |- ( ( A e. V /\ A. x e. A K e. Top ) -> X_ x e. A U. K = U. J )
Theorem	pttopon 20182*	The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- J = ( Xt_ ` ( x e. A |-> K ) )   =>    |- ( ( A e. V /\ A. x e. A K e. (TopOn ` B ) ) -> J e. (TopOn ` X_ x e. A B ) )
Theorem	pttoponconst 20183	The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- J = ( Xt_ ` ( A X. { R } ) )   =>    |- ( ( A e. V /\ R e. (TopOn ` X ) ) -> J e. (TopOn ` ( X ^m A ) ) )
Theorem	ptuniconst 20184	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 20185	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 20186	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 20187*	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 20188	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 20189	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 20190	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 20191	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 20192	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 20193	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 20194*	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 20195	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 20196	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 20197*	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 20198*	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 20199*	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 20200*	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 ) ) ) )