P. 227 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22601-22700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	kgentop 22601	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 22602	The compact generator generates a finer topology than the original. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝐽 ∈ Top → 𝐽 ⊆ (𝑘Gen‘𝐽))
Theorem	kgenhaus 22603	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 22604	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 22605	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 22606	The compact generator is idempotent on compactly generated spaces. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝐽 ∈ ran 𝑘Gen → (𝑘Gen‘𝐽) = 𝐽)
Theorem	iskgen2 22607	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 22608*	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 22609*	A locally compact space is compactly generated. (This variant of llycmpkgen 22611 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 22610	A compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ Comp → 𝐽 ∈ ran 𝑘Gen)
Theorem	llycmpkgen 22611	A locally compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ ran 𝑘Gen)
Theorem	1stckgenlem 22612	The one-point compactification of ℕ is compact. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐴)    ⇒   ⊢ (𝜑 → (𝐽 ↾t (ran 𝐹 ∪ {𝐴})) ∈ Comp)
Theorem	1stckgen 22613	A first-countable space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 1stω → 𝐽 ∈ ran 𝑘Gen)
Theorem	kgen2ss 22614	The compact generator preserves the subset (fineness) relationship on topologies. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝑘Gen‘𝐽) ⊆ (𝑘Gen‘𝐾))
Theorem	kgencn 22615*	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 22616*	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 22617	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 22618	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 22619	Extend class notation with the binary topological product operation.
class ×t
Syntax	cxko 22620	Extend class notation with a function whose value is the compact-open topology.
class ↑ko
Definition	df-tx 22621*	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 22622*	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 22623*	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 22624*	The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))    &   ⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝑌 = ∪ 𝑆    ⇒   ⊢ (𝑋 × 𝑌) = ∪ 𝐵
Theorem	txbasex 22625*	The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝐵 ∈ V)
Theorem	txbas 22626*	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 22627*	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 22628	The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
Theorem	ptval 22629*	The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (∏t‘𝐹) = (topGen‘𝐵))
Theorem	ptpjpre1 22630*	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 22631*	Elementhood in the bases of a product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ (𝑆 ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑆 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)))
Theorem	elptr 22632*	A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ 𝐵)
Theorem	elptr2 22633*	A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ 𝐵)
Theorem	ptbasid 22634*	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 22635*	The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐵)
Theorem	ptbasin 22636*	The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∩ 𝑌) ∈ 𝐵)
Theorem	ptbasin2 22637*	The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
Theorem	ptbas 22638*	The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
Theorem	ptpjpre2 22639*	The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}    &   ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝐼 ∈ 𝐴 ∧ 𝑈 ∈ (𝐹‘𝐼))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝐼)) “ 𝑈) ∈ 𝐵)
Theorem	ptbasfi 22640*	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 22641	The product topology is a topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∏t‘𝐹) ∈ Top)
Theorem	ptopn 22642*	A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Top)    &   ⊢ (𝜑 → 𝑊 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ (∏t‘𝐹))
Theorem	ptopn2 22643*	A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Top)    &   ⊢ (𝜑 → 𝑂 ∈ (𝐹‘𝑌))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝐴 if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) ∈ (∏t‘𝐹))
Theorem	xkotf 22644*	Functionality of function 𝑇. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}    &   ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})    ⇒   ⊢ 𝑇:(𝐾 × 𝑆)⟶𝒫 (𝑅 Cn 𝑆)
Theorem	xkobval 22645*	Alternative expression for the subbase of the compact-open topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}    &   ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})    ⇒   ⊢ ran 𝑇 = {𝑠 ∣ ∃𝑘 ∈ 𝒫 𝑋∃𝑣 ∈ 𝑆 ((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑠 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})}
Theorem	xkoval 22646*	Value of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp}    &   ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})    ⇒   ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) = (topGen‘(fi‘ran 𝑇)))
Theorem	xkotop 22647	The compact-open topology is a topology. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top)
Theorem	xkoopn 22648*	A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ (𝜑 → 𝑅 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑅 ↾t 𝐴) ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑆)    ⇒   ⊢ (𝜑 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ (𝑆 ↑ko 𝑅))
Theorem	txtopi 22649	The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ 𝑅 ∈ Top    &   ⊢ 𝑆 ∈ Top    ⇒   ⊢ (𝑅 ×t 𝑆) ∈ Top
Theorem	txtopon 22650	The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)))
Theorem	txuni 22651	The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝑌 = ∪ 𝑆    ⇒   ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆))
Theorem	txunii 22652	The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.)
⊢ 𝑅 ∈ Top    &   ⊢ 𝑆 ∈ Top    &   ⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝑌 = ∪ 𝑆    ⇒   ⊢ (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)
Theorem	ptuni 22653*	The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐽 = (∏t‘𝐹)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑥 ∈ 𝐴 ∪ (𝐹‘𝑥) = ∪ 𝐽)
Theorem	ptunimpt 22654*	Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐴 ↦ 𝐾))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐾 ∈ Top) → X𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ 𝐽)
Theorem	pttopon 22655*	The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐴 ↦ 𝐾))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐾 ∈ (TopOn‘𝐵)) → 𝐽 ∈ (TopOn‘X𝑥 ∈ 𝐴 𝐵))
Theorem	pttoponconst 22656	The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ 𝐽 = (∏t‘(𝐴 × {𝑅}))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ (TopOn‘𝑋)) → 𝐽 ∈ (TopOn‘(𝑋 ↑m 𝐴)))
Theorem	ptuniconst 22657	The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ 𝐽 = (∏t‘(𝐴 × {𝑅}))    &   ⊢ 𝑋 = ∪ 𝑅    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ Top) → (𝑋 ↑m 𝐴) = ∪ 𝐽)
Theorem	xkouni 22658	The base set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝐽 = (𝑆 ↑ko 𝑅)    ⇒   ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ 𝐽)
Theorem	xkotopon 22659	The base set of the compact-open topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ 𝐽 = (𝑆 ↑ko 𝑅)    ⇒   ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 ∈ (TopOn‘(𝑅 Cn 𝑆)))
Theorem	ptval2 22660*	The value of the product topology function. (Contributed by Mario Carneiro, 7-Feb-2015.)
⊢ 𝐽 = (∏t‘𝐹)    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐺 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐽 = (topGen‘(fi‘({𝑋} ∪ ran 𝐺))))
Theorem	txopn 22661	The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴 × 𝐵) ∈ (𝑅 ×t 𝑆))
Theorem	txcld 22662	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.)
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (𝐴 × 𝐵) ∈ (Clsd‘(𝑅 ×t 𝑆)))
Theorem	txcls 22663	Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
Theorem	txss12 22664	Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)) → (𝐴 ×t 𝐶) ⊆ (𝐵 ×t 𝐷))
Theorem	txbasval 22665	It is sufficient to consider products of the bases for the topologies in the topological product. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ((topGen‘𝑅) ×t (topGen‘𝑆)) = (𝑅 ×t 𝑆))
Theorem	neitx 22666	The Cartesian product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)))
Theorem	txcnpi 22667*	Continuity of a two-argument function at a point. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘⟨𝐴, 𝐵⟩))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈)))
Theorem	tx1cn 22668	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.)
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
Theorem	tx2cn 22669	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.)
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
Theorem	ptpjcn 22670*	Continuity of a projection map into a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Feb-2015.)
⊢ 𝑌 = ∪ 𝐽    &   ⊢ 𝐽 = (∏t‘𝐹)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐼 ∈ 𝐴) → (𝑥 ∈ 𝑌 ↦ (𝑥‘𝐼)) ∈ (𝐽 Cn (𝐹‘𝐼)))
Theorem	ptpjopn 22671*	The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑌 = ∪ 𝐽    &   ⊢ 𝐽 = (∏t‘𝐹)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐼 ∈ 𝐴) ∧ 𝑈 ∈ 𝐽) → ((𝑥 ∈ 𝑌 ↦ (𝑥‘𝐼)) “ 𝑈) ∈ (𝐹‘𝐼))
Theorem	ptcld 22672*	A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Top)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (Clsd‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝐶 ∈ (Clsd‘(∏t‘𝐹)))
Theorem	ptcldmpt 22673*	A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝐶 ∈ (Clsd‘(∏t‘(𝑘 ∈ 𝐴 ↦ 𝐽))))
Theorem	ptclsg 22674*	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.)
⊢ 𝐽 = (∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑅 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝑆 ∈ AC 𝐴)    ⇒   ⊢ (𝜑 → ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆) = X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆))
Theorem	ptcls 22675*	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.)
⊢ 𝐽 = (∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑅 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆) = X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆))
Theorem	dfac14lem 22676*	Lemma for dfac14 22677. By equipping 𝑆 ∪ {𝑃} for some 𝑃 ∉ 𝑆 with the particular point topology, we can show that 𝑃 is in the closure of 𝑆; hence the sequence 𝑃(𝑥) is in the product of the closures, and we can utilize this instance of ptcls 22675 to extract an element of the closure of X𝑘 ∈ 𝐼𝑆. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)    &   ⊢ 𝑃 = 𝒫 ∪ 𝑆    &   ⊢ 𝑅 = {𝑦 ∈ 𝒫 (𝑆 ∪ {𝑃}) ∣ (𝑃 ∈ 𝑦 → 𝑦 = (𝑆 ∪ {𝑃}))}    &   ⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ (𝜑 → ((cls‘𝐽)‘X𝑥 ∈ 𝐼 𝑆) = X𝑥 ∈ 𝐼 ((cls‘𝑅)‘𝑆))    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)
Theorem	dfac14 22677*	Theorem ptcls 22675 is an equivalent of the axiom of choice. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘))))
Theorem	xkoccn 22678*	The "constant function" function which maps 𝑥 ∈ 𝑌 to the constant function 𝑧 ∈ 𝑋 ↦ 𝑥 is a continuous function from 𝑋 into the space of continuous functions from 𝑌 to 𝑋. This can also be understood as the currying of the first projection function. (The currying of the second projection function is 𝑥 ∈ 𝑌 ↦ (𝑧 ∈ 𝑋 ↦ 𝑧), which we already know is continuous because it is a constant function.) (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) ∈ (𝑆 Cn (𝑆 ↑ko 𝑅)))
Theorem	txcnp 22679*	If two functions are continuous at 𝐷, then the ordered pair of them is continuous at 𝐷 into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩) ∈ ((𝐽 CnP (𝐾 ×t 𝐿))‘𝐷))
Theorem	ptcnplem 22680*	Lemma for ptcnp 22681. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ 𝐾 = (∏t‘𝐹)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶Top)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))    &   ⊢ Ⅎ𝑘𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐺 Fn 𝐼)    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ Fin)    &   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘))    &   ⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘)))
Theorem	ptcnp 22681*	If every projection of a function is continuous at 𝐷, then the function itself is continuous at 𝐷 into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ 𝐾 = (∏t‘𝐹)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶Top)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷))
Theorem	upxp 22682*	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.)
⊢ 𝑃 = (1st ↾ (𝐵 × 𝐶))    &   ⊢ 𝑄 = (2nd ↾ (𝐵 × 𝐶))    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ∃!ℎ(ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))
Theorem	txcnmpt 22683*	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.)
⊢ 𝑊 = ∪ 𝑈    &   ⊢ 𝐻 = (𝑥 ∈ 𝑊 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩)    ⇒   ⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐻 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
Theorem	uptx 22684*	Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
⊢ 𝑇 = (𝑅 ×t 𝑆)    &   ⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝑌 = ∪ 𝑆    &   ⊢ 𝑍 = (𝑋 × 𝑌)    &   ⊢ 𝑃 = (1st ↾ 𝑍)    &   ⊢ 𝑄 = (2nd ↾ 𝑍)    ⇒   ⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn 𝑇)(𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))
Theorem	txcn 22685	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.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝑌 = ∪ 𝑆    &   ⊢ 𝑍 = (𝑋 × 𝑌)    &   ⊢ 𝑊 = ∪ 𝑈    &   ⊢ 𝑃 = (1st ↾ 𝑍)    &   ⊢ 𝑄 = (2nd ↾ 𝑍)    ⇒   ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
Theorem	ptcn 22686*	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.)
⊢ 𝐾 = (∏t‘𝐹)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶Top)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn (𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ (𝐽 Cn 𝐾))
Theorem	prdstopn 22687	Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ 𝑂 = (TopOpen‘𝑌)    ⇒   ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
Theorem	prdstps 22688	A structure product of topological spaces is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶TopSp)    ⇒   ⊢ (𝜑 → 𝑌 ∈ TopSp)
Theorem	pwstps 22689	A structure power of a topological space is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ TopSp ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ TopSp)
Theorem	txrest 22690	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.)
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑅 ×t 𝑆) ↾t (𝐴 × 𝐵)) = ((𝑅 ↾t 𝐴) ×t (𝑆 ↾t 𝐵)))
Theorem	txdis 22691	The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝒫 𝐴 ×t 𝒫 𝐵) = 𝒫 (𝐴 × 𝐵))
Theorem	txindislem 22692	Lemma for txindis 22693. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (( I ‘𝐴) × ( I ‘𝐵)) = ( I ‘(𝐴 × 𝐵))
Theorem	txindis 22693	The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ({∅, 𝐴} ×t {∅, 𝐵}) = {∅, (𝐴 × 𝐵)}
Theorem	txdis1cn 22694*	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.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐾 ∈ Top)    &   ⊢ (𝜑 → 𝐹 Fn (𝑋 × 𝑌))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾))
Theorem	txlly 22695*	If the property 𝐴 is preserved under topological products, then so is the property of being locally 𝐴. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×t 𝑘) ∈ 𝐴)    ⇒   ⊢ ((𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴) → (𝑅 ×t 𝑆) ∈ Locally 𝐴)
Theorem	txnlly 22696*	If the property 𝐴 is preserved under topological products, then so is the property of being n-locally 𝐴. (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×t 𝑘) ∈ 𝐴)    ⇒   ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×t 𝑆) ∈ 𝑛-Locally 𝐴)
Theorem	pthaus 22697	The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) → (∏t‘𝐹) ∈ Haus)
Theorem	ptrescn 22698*	Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐽 = (∏t‘𝐹)    &   ⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐵))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐽 Cn 𝐾))
Theorem	txtube 22699*	The "tube lemma". If 𝑋 is compact and there is an open set 𝑈 containing the line 𝑋 × {𝐴}, then there is a "tube" 𝑋 × 𝑢 for some neighborhood 𝑢 of 𝐴 which is entirely contained within 𝑈. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝑌 = ∪ 𝑆    &   ⊢ (𝜑 → 𝑅 ∈ Comp)    &   ⊢ (𝜑 → 𝑆 ∈ Top)    &   ⊢ (𝜑 → 𝑈 ∈ (𝑅 ×t 𝑆))    &   ⊢ (𝜑 → (𝑋 × {𝐴}) ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))
Theorem	txcmplem1 22700*	Lemma for txcmp 22702. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝑌 = ∪ 𝑆    &   ⊢ (𝜑 → 𝑅 ∈ Comp)    &   ⊢ (𝜑 → 𝑆 ∈ Comp)    &   ⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆))    &   ⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑢) ⊆ ∪ 𝑣))