P. 235 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23401-23500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	llyrest 23401	An open subspace of a locally 𝐴 space is also locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽) → (𝐽 ↾t 𝐵) ∈ Locally 𝐴)
Theorem	nllyrest 23402	An open subspace of an n-locally 𝐴 space is also n-locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽) → (𝐽 ↾t 𝐵) ∈ 𝑛-Locally 𝐴)
Theorem	loclly 23403	If 𝐴 is a local property, then both Locally 𝐴 and 𝑛-Locally 𝐴 simplify to 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (Locally 𝐴 = 𝐴 ↔ 𝑛-Locally 𝐴 = 𝐴)
Theorem	llyidm 23404	Idempotence of the "locally" predicate, i.e. being "locally 𝐴 " is a local property. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ Locally Locally 𝐴 = Locally 𝐴
Theorem	nllyidm 23405	Idempotence of the "n-locally" predicate, i.e. being "n-locally 𝐴 " is a local property. (Use loclly 23403 to show 𝑛-Locally 𝑛-Locally 𝐴 = 𝑛-Locally 𝐴.) (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ Locally 𝑛-Locally 𝐴 = 𝑛-Locally 𝐴
Theorem	toplly 23406	A topology is locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ Locally Top = Top
Theorem	topnlly 23407	A topology is n-locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝑛-Locally Top = Top
Theorem	hauslly 23408	A Hausdorff space is locally Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Locally Haus)
Theorem	hausnlly 23409	A Hausdorff space is n-locally Hausdorff iff it is locally Hausdorff (both notions are thus referred to as "locally Hausdorff"). (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ 𝑛-Locally Haus ↔ 𝐽 ∈ Locally Haus)
Theorem	hausllycmp 23410	A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) → 𝐽 ∈ 𝑛-Locally Comp)
Theorem	cldllycmp 23411	A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest 23402.) (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ 𝑛-Locally Comp)
Theorem	lly1stc 23412	First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ Locally 1stω = 1stω
Theorem	dislly 23413*	The discrete space 𝒫 𝑋 is locally 𝐴 if and only if every singleton space has property 𝐴. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝑋 ∈ 𝑉 → (𝒫 𝑋 ∈ Locally 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝒫 {𝑥} ∈ 𝐴))
Theorem	disllycmp 23414	A discrete space is locally compact. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Locally Comp)
Theorem	dis1stc 23415	A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ 1stω)
Theorem	hausmapdom 23416	If 𝑋 is a first-countable Hausdorff space, then the cardinality of the closure of a set 𝐴 is bounded by ℕ to the power 𝐴. In particular, a first-countable Hausdorff space with a dense subset 𝐴 has cardinality at most 𝐴↑ℕ, and a separable first-countable Hausdorff space has cardinality at most 𝒫 ℕ. (Compare hauspwpwdom 23904 to see a weaker result if the assumption of first-countability is omitted.) (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑m ℕ))
Theorem	hauspwdom 23417	Simplify the cardinal 𝐴↑ℕ of hausmapdom 23416 to 𝒫 𝐵 = 2↑𝐵 when 𝐵 is an infinite cardinal greater than 𝐴. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵)
12.1.16  Refinements
Syntax	cref 23418	Extend class definition to include the refinement relation.
class Ref
Syntax	cptfin 23419	Extend class definition to include the class of point-finite covers.
class PtFin
Syntax	clocfin 23420	Extend class definition to include the class of locally finite covers.
class LocFin
Definition	df-ref 23421*	Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.)
⊢ Ref = {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)}
Definition	df-ptfin 23422*	Define "point-finite." (Contributed by Jeff Hankins, 21-Jan-2010.)
⊢ PtFin = {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin}
Definition	df-locfin 23423*	Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
⊢ LocFin = (𝑥 ∈ Top ↦ {𝑦 ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))})
Theorem	refrel 23424	Refinement is a relation. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
⊢ Rel Ref
Theorem	isref 23425*	The property of being a refinement of a cover. Dr. Nyikos once commented in class that the term "refinement" is actually misleading and that people are inclined to confuse it with the notion defined in isfne 36404. On the other hand, the two concepts do seem to have a dual relationship. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐴 ∈ 𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)))
Theorem	refbas 23426	A refinement covers the same set. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐴Ref𝐵 → 𝑌 = 𝑋)
Theorem	refssex 23427*	Every set in a refinement has a superset in the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
⊢ ((𝐴Ref𝐵 ∧ 𝑆 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 𝑆 ⊆ 𝑥)
Theorem	ssref 23428	A subcover is a refinement of the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌) → 𝐴Ref𝐵)
Theorem	refref 23429	Reflexivity of refinement. (Contributed by Jeff Hankins, 18-Jan-2010.)
⊢ (𝐴 ∈ 𝑉 → 𝐴Ref𝐴)
Theorem	reftr 23430	Refinement is transitive. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.)
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → 𝐴Ref𝐶)
Theorem	refun0 23431	Adding the empty set preserves refinements. (Contributed by Thierry Arnoux, 31-Jan-2020.)
⊢ ((𝐴Ref𝐵 ∧ 𝐵 ≠ ∅) → (𝐴 ∪ {∅})Ref𝐵)
Theorem	isptfin 23432*	The statement "is a point-finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.)
⊢ 𝑋 = ∪ 𝐴    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ PtFin ↔ ∀𝑥 ∈ 𝑋 {𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦} ∈ Fin))
Theorem	islocfin 23433*	The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐴    ⇒   ⊢ (𝐴 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)))
Theorem	finptfin 23434	A finite cover is a point-finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.)
⊢ (𝐴 ∈ Fin → 𝐴 ∈ PtFin)
Theorem	ptfinfin 23435*	A point covered by a point-finite cover is only covered by finitely many elements. (Contributed by Jeff Hankins, 21-Jan-2010.)
⊢ 𝑋 = ∪ 𝐴    ⇒   ⊢ ((𝐴 ∈ PtFin ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥} ∈ Fin)
Theorem	finlocfin 23436	A finite cover of a topological space is a locally finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐴    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐴 ∈ (LocFin‘𝐽))
Theorem	locfintop 23437	A locally finite cover covers a topological space. (Contributed by Jeff Hankins, 21-Jan-2010.)
⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
Theorem	locfinbas 23438	A locally finite cover must cover the base set of its corresponding topological space. (Contributed by Jeff Hankins, 21-Jan-2010.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐴    ⇒   ⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝑋 = 𝑌)
Theorem	locfinnei 23439*	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.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝑃 ∈ 𝑋) → ∃𝑛 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))
Theorem	lfinpfin 23440	A locally finite cover is point-finite. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐴 ∈ PtFin)
Theorem	lfinun 23441	Adding a finite set preserves locally finite covers. (Contributed by Thierry Arnoux, 31-Jan-2020.)
⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵 ⊆ ∪ 𝐽) → (𝐴 ∪ 𝐵) ∈ (LocFin‘𝐽))
Theorem	locfincmp 23442	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.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐶    ⇒   ⊢ (𝐽 ∈ Comp → (𝐶 ∈ (LocFin‘𝐽) ↔ (𝐶 ∈ Fin ∧ 𝑋 = 𝑌)))
Theorem	unisngl 23443*	Taking the union of the set of singletons recovers the initial set. (Contributed by Thierry Arnoux, 9-Jan-2020.)
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}}    ⇒   ⊢ 𝑋 = ∪ 𝐶
Theorem	dissnref 23444*	The set of singletons is a refinement of any open covering of the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.)
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}}    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → 𝐶Ref𝑌)
Theorem	dissnlocfin 23445*	The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.)
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}}    ⇒   ⊢ (𝑋 ∈ 𝑉 → 𝐶 ∈ (LocFin‘𝒫 𝑋))
Theorem	locfindis 23446	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.)
⊢ 𝑌 = ∪ 𝐶    ⇒   ⊢ (𝐶 ∈ (LocFin‘𝒫 𝑋) ↔ (𝐶 ∈ PtFin ∧ 𝑋 = 𝑌))
Theorem	locfincf 23447	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.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (LocFin‘𝐽) ⊆ (LocFin‘𝐾))
Theorem	comppfsc 23448*	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.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))
12.1.17  Compactly generated spaces
Syntax	ckgen 23449	Extend class notation with the compact generator operation.
class 𝑘Gen
Definition	df-kgen 23450*	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. 𝑥 ∈ (𝑘Gen‘𝑗), iff the preimage of 𝑥 is open in all compact Hausdorff spaces. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))})
Theorem	kgenval 23451*	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.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑘Gen‘𝐽) = {𝑥 ∈ 𝒫 𝑋 ∣ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))})
Theorem	elkgen 23452*	Value of the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐴 ∈ (𝑘Gen‘𝐽) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐴 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)))))
Theorem	kgeni 23453	Property of the open sets in the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ ((𝐴 ∈ (𝑘Gen‘𝐽) ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐴 ∩ 𝐾) ∈ (𝐽 ↾t 𝐾))
Theorem	kgentopon 23454	The compact generator generates a topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑘Gen‘𝐽) ∈ (TopOn‘𝑋))
Theorem	kgenuni 23455	The base set of the compact generator is the same as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → 𝑋 = ∪ (𝑘Gen‘𝐽))
Theorem	kgenftop 23456	The compact generator generates a topology. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝐽 ∈ Top → (𝑘Gen‘𝐽) ∈ Top)
Theorem	kgenf 23457	The compact generator is a function on topologies. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝑘Gen:Top⟶Top
Theorem	kgentop 23458	A compactly generated space is a topology. (Note: henceforth we will use the idiom "𝐽 ∈ ran 𝑘Gen " to denote "𝐽 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.)
⊢ (𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top)
Theorem	kgenss 23459	The compact generator generates a finer topology than the original. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝐽 ∈ Top → 𝐽 ⊆ (𝑘Gen‘𝐽))
Theorem	kgenhaus 23460	The compact generator generates another Hausdorff topology given a Hausdorff topology to start from. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ Haus → (𝑘Gen‘𝐽) ∈ Haus)
Theorem	kgencmp 23461	The compact generator topology is the same as the original topology on compact subspaces. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) = ((𝑘Gen‘𝐽) ↾t 𝐾))
Theorem	kgencmp2 23462	The compact generator topology has the same compact sets as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝐽 ∈ Top → ((𝐽 ↾t 𝐾) ∈ Comp ↔ ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp))
Theorem	kgenidm 23463	The compact generator is idempotent on compactly generated spaces. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝐽 ∈ ran 𝑘Gen → (𝑘Gen‘𝐽) = 𝐽)
Theorem	iskgen2 23464	A space is compactly generated iff it contains its image under the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝐽 ∈ ran 𝑘Gen ↔ (𝐽 ∈ Top ∧ (𝑘Gen‘𝐽) ⊆ 𝐽))
Theorem	iskgen3 23465*	Derive the usual definition of "compactly generated". A topology is compactly generated if every subset of 𝑋 that is open in every compact subset is open. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ ran 𝑘Gen ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫 𝑋(∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) → 𝑥 ∈ 𝐽)))
Theorem	llycmpkgen2 23466*	A locally compact space is compactly generated. (This variant of llycmpkgen 23468 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.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑘 ∈ ((nei‘𝐽)‘{𝑥})(𝐽 ↾t 𝑘) ∈ Comp)    ⇒   ⊢ (𝜑 → 𝐽 ∈ ran 𝑘Gen)
Theorem	cmpkgen 23467	A compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ Comp → 𝐽 ∈ ran 𝑘Gen)
Theorem	llycmpkgen 23468	A locally compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ ran 𝑘Gen)
Theorem	1stckgenlem 23469	The one-point compactification of ℕ is compact. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐴)    ⇒   ⊢ (𝜑 → (𝐽 ↾t (ran 𝐹 ∪ {𝐴})) ∈ Comp)
Theorem	1stckgen 23470	A first-countable space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 1stω → 𝐽 ∈ ran 𝑘Gen)
Theorem	kgen2ss 23471	The compact generator preserves the subset (fineness) relationship on topologies. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝑘Gen‘𝐽) ⊆ (𝑘Gen‘𝐾))
Theorem	kgencn 23472*	A function from a compactly generated space is continuous iff it is continuous "on compacta". (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ ((𝑘Gen‘𝐽) Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾)))))
Theorem	kgencn2 23473*	A function 𝐹:𝐽⟶𝐾 from a compactly generated space is continuous iff for all compact spaces 𝑧 and continuous 𝑔:𝑧⟶𝐽, the composite 𝐹 ∘ 𝑔:𝑧⟶𝐾 is continuous. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ ((𝑘Gen‘𝐽) Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑧 ∈ Comp ∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾))))
Theorem	kgencn3 23474	The set of continuous functions from 𝐽 to 𝐾 is unaffected by k-ification of 𝐾, if 𝐽 is already compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝑘Gen‘𝐾)))
Theorem	kgen2cn 23475	A continuous function is also continuous with the domain and codomain replaced by their compact generator topologies. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 ∈ ((𝑘Gen‘𝐽) Cn (𝑘Gen‘𝐾)))
12.1.18  Product topologies
Syntax	ctx 23476	Extend class notation with the binary topological product operation.
class ×t
Syntax	cxko 23477	Extend class notation with a function whose value is the compact-open topology.
class ↑ko
Definition	df-tx 23478*	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.)
⊢ ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))
Definition	df-xko 23479*	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 = (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
Theorem	txval 23480*	Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝑅 ×t 𝑆) = (topGen‘𝐵))
Theorem	txuni2 23481*	The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))    &   ⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝑌 = ∪ 𝑆    ⇒   ⊢ (𝑋 × 𝑌) = ∪ 𝐵
Theorem	txbasex 23482*	The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝐵 ∈ V)
Theorem	txbas 23483*	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.)
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ TopBases)
Theorem	eltx 23484*	A set in a product is open iff each point is surrounded by an open rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊) → (𝑆 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑝 ∈ 𝑆 ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐾 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝑆)))
Theorem	txtop 23485	The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
Theorem	ptval 23486*	The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (∏t‘𝐹) = (topGen‘𝐵))
Theorem	ptpjpre1 23487*	The preimage of a projection function can be expressed as an indexed cartesian product. (Contributed by Mario Carneiro, 6-Feb-2015.)
⊢ 𝑋 = X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝐼 ∈ 𝐴 ∧ 𝑈 ∈ (𝐹‘𝐼))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝐼)) “ 𝑈) = X𝑘 ∈ 𝐴 if(𝑘 = 𝐼, 𝑈, ∪ (𝐹‘𝑘)))
Theorem	elpt 23488*	Elementhood in the bases of a product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ (𝑆 ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑆 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)))
Theorem	elptr 23489*	A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ 𝐵)
Theorem	elptr2 23490*	A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ 𝐵)
Theorem	ptbasid 23491*	The base set of the product topology is a basic open set. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∈ 𝐵)
Theorem	ptuni2 23492*	The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐵)
Theorem	ptbasin 23493*	The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∩ 𝑌) ∈ 𝐵)
Theorem	ptbasin2 23494*	The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
Theorem	ptbas 23495*	The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
Theorem	ptpjpre2 23496*	The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    &   ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝐼 ∈ 𝐴 ∧ 𝑈 ∈ (𝐹‘𝐼))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝐼)) “ 𝑈) ∈ 𝐵)
Theorem	ptbasfi 23497*	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 𝑋 itself to the list because if 𝐴 is empty we get (fi‘∅) = ∅ while 𝐵 = {∅}.) (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    &   ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
Theorem	pttop 23498	The product topology is a topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∏t‘𝐹) ∈ Top)
Theorem	ptopn 23499*	A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Top)    &   ⊢ (𝜑 → 𝑊 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ (∏t‘𝐹))
Theorem	ptopn2 23500*	A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Top)    &   ⊢ (𝜑 → 𝑂 ∈ (𝐹‘𝑌))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝐴 if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) ∈ (∏t‘𝐹))