P. 237 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23601-23700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnmpt1t 23601*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ⟨𝐴, 𝐵⟩) ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
Theorem	cnmpt12f 23602*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐾 ×t 𝐿) Cn 𝑀))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝐽 Cn 𝑀))
Theorem	cnmpt12 23603*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐶) ∈ ((𝐾 ×t 𝐿) Cn 𝑀))    &   ⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐷) ∈ (𝐽 Cn 𝑀))
Theorem	cnmpt1st 23604*	The projection onto the first coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
Theorem	cnmpt2nd 23605*	The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾))
Theorem	cnmpt2c 23606*	A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑃) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
Theorem	cnmpt21 23607*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀))    &   ⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
Theorem	cnmpt21f 23608*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐿 Cn 𝑀))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐹‘𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))
Theorem	cnmpt2t 23609*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨𝐴, 𝐵⟩) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀)))
Theorem	cnmpt22 23610*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊))    &   ⊢ (𝜑 → (𝑧 ∈ 𝑍, 𝑤 ∈ 𝑊 ↦ 𝐶) ∈ ((𝐿 ×t 𝑀) Cn 𝑁))    &   ⊢ ((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐷) ∈ ((𝐽 ×t 𝐾) Cn 𝑁))
Theorem	cnmpt22f 23611*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐿 ×t 𝑀) Cn 𝑁))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴𝐹𝐵)) ∈ ((𝐽 ×t 𝐾) Cn 𝑁))
Theorem	cnmpt1res 23612*	The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.)
⊢ 𝐾 = (𝐽 ↾t 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐿))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿))
Theorem	cnmpt2res 23613*	The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ 𝐾 = (𝐽 ↾t 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ 𝑁 = (𝑀 ↾t 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → 𝑊 ⊆ 𝑍)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑍 ↦ 𝐴) ∈ ((𝐽 ×t 𝑀) Cn 𝐿))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑌, 𝑦 ∈ 𝑊 ↦ 𝐴) ∈ ((𝐾 ×t 𝑁) Cn 𝐿))
Theorem	cnmptcom 23614*	The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐾 ×t 𝐽) Cn 𝐿))
Theorem	cnmptkc 23615*	The curried first projection function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝑥)) ∈ (𝐽 Cn (𝐽 ↑ko 𝐾)))
Theorem	cnmptkp 23616*	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.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿))
Theorem	cnmptk1 23617*	The composition of a curried function with a one-arg function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))    &   ⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀))    &   ⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐾)))
Theorem	cnmpt1k 23618*	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.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐿))    &   ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ (𝑧 ∈ 𝑍 ↦ 𝐵)) ∈ (𝐾 Cn (𝑀 ↑ko 𝐿)))    &   ⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ (𝑥 ∈ 𝑋 ↦ 𝐶)) ∈ (𝐾 Cn (𝑀 ↑ko 𝐽)))
Theorem	cnmptkk 23619*	The composition of two curried functions is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑛-Locally Comp)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑧 ∈ 𝑍 ↦ 𝐵)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐿)))    &   ⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐾)))
Theorem	xkofvcn 23620*	Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn 23592.) (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝐹 = (𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))    ⇒   ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top) → 𝐹 ∈ (((𝑆 ↑ko 𝑅) ×t 𝑅) Cn 𝑆))
Theorem	cnmptk1p 23621*	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.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿))
Theorem	cnmptk2 23622*	The uncurrying of a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
Theorem	xkoinjcn 23623*	Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ⟨𝑦, 𝑥⟩))    ⇒   ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝐹 ∈ (𝑅 Cn ((𝑆 ×t 𝑅) ↑ko 𝑆)))
Theorem	cnmpt2k 23624*	The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
Theorem	txconn 23625	The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.)
⊢ ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Conn)
Theorem	imasnopn 23626	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.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ∈ 𝐾)
Theorem	imasncld 23627	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.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ∈ (Clsd‘𝐾))
Theorem	imasncls 23628	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.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ⊆ (𝑋 × 𝑌) ∧ 𝐴 ∈ 𝑋)) → ((cls‘𝐾)‘(𝑅 “ {𝐴})) ⊆ (((cls‘(𝐽 ×t 𝐾))‘𝑅) “ {𝐴}))
12.1.20  Quotient maps and quotient topology
Syntax	ckq 23629	Extend class notation with the Kolmogorov quotient function.
class KQ
Definition	df-kq 23630*	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 = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦})))
Theorem	qtopval 23631*	Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽})
Theorem	qtopval2 23632*	Value of the quotient topology function when 𝐹 is a function on the base set. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽})
Theorem	elqtop 23633	Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽)))
Theorem	qtopres 23634	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 𝐹 be a function with domain 𝑋. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋)))
Theorem	qtoptop2 23635	The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐽 qTop 𝐹) ∈ Top)
Theorem	qtoptop 23636	The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
Theorem	elqtop2 23637	Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽)))
Theorem	qtopuni 23638	The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹))
Theorem	elqtop3 23639	Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽)))
Theorem	qtoptopon 23640	The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
Theorem	qtopid 23641	A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
Theorem	idqtop 23642	The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 qTop ( I ↾ 𝑋)) = 𝐽)
Theorem	qtopcmplem 23643	Lemma for qtopcmp 23644 and qtopconn 23645. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top)    &   ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹:𝑋–onto→∪ (𝐽 qTop 𝐹) ∧ 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) → (𝐽 qTop 𝐹) ∈ 𝐴)    ⇒   ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ 𝐴)
Theorem	qtopcmp 23644	A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Comp)
Theorem	qtopconn 23645	A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Conn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Conn)
Theorem	qtopkgen 23646	A quotient of a compactly generated space is compactly generated. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ ran 𝑘Gen)
Theorem	basqtop 23647	An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝐽 qTop 𝐹) ∈ TopBases)
Theorem	tgqtop 23648	An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ((topGen‘𝐽) qTop 𝐹) = (topGen‘(𝐽 qTop 𝐹)))
Theorem	qtopcld 23649	The property of being a closed set in the quotient topology. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽))))
Theorem	qtopcn 23650	Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾)))
Theorem	qtopss 23651	A surjective continuous function from 𝐽 to 𝐾 induces a topology 𝐽 qTop 𝐹 on the base set of 𝐾. This topology is in general finer than 𝐾. Together with qtopid 23641, this implies that 𝐽 qTop 𝐹 is the finest topology making 𝐹 continuous, i.e. the final topology with respect to the family {𝐹}. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 = 𝑌) → 𝐾 ⊆ (𝐽 qTop 𝐹))
Theorem	qtopeu 23652*	Universal property of the quotient topology. If 𝐺 is a function from 𝐽 to 𝐾 which is equal on all equivalent elements under 𝐹, then there is a unique continuous map 𝑓:(𝐽 / 𝐹)⟶𝐾 such that 𝐺 = 𝑓 ∘ 𝐹, and we say that 𝐺 "passes to the quotient". (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐺‘𝑥) = (𝐺‘𝑦))    ⇒   ⊢ (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹))
Theorem	qtoprest 23653	If 𝐴 is a saturated open or closed set (where saturated means that 𝐴 = (◡𝐹 “ 𝑈) for some 𝑈), then the restriction of the quotient map 𝐹 to 𝐴 is a quotient map. (Contributed by Mario Carneiro, 24-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑌)    &   ⊢ (𝜑 → 𝐴 = (◡𝐹 “ 𝑈))    &   ⊢ (𝜑 → (𝐴 ∈ 𝐽 ∨ 𝐴 ∈ (Clsd‘𝐽)))    ⇒   ⊢ (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽 ↾t 𝐴) qTop (𝐹 ↾ 𝐴)))
Theorem	qtopomap 23654*	If 𝐹 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.)
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → ran 𝐹 = 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾)    ⇒   ⊢ (𝜑 → 𝐾 = (𝐽 qTop 𝐹))
Theorem	qtopcmap 23655*	If 𝐹 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.)
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → ran 𝐹 = 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑥) ∈ (Clsd‘𝐾))    ⇒   ⊢ (𝜑 → 𝐾 = (𝐽 qTop 𝐹))
Theorem	imastopn 23656	The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝑂 = (TopOpen‘𝑈)    ⇒   ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹))
Theorem	imastps 23657	The image of a topological space under a function is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ TopSp)    ⇒   ⊢ (𝜑 → 𝑈 ∈ TopSp)
Theorem	qustps 23658	A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s 𝐸))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ TopSp)    ⇒   ⊢ (𝜑 → 𝑈 ∈ TopSp)
Theorem	kqfval 23659*	Value of the function appearing in df-kq 23630. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) = {𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦})
Theorem	kqfeq 23660*	Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐹‘𝐴) = (𝐹‘𝐵) ↔ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ↔ 𝐵 ∈ 𝑦)))
Theorem	kqffn 23661*	The topological indistinguishability map is a function on the base. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ 𝑉 → 𝐹 Fn 𝑋)
Theorem	kqval 23662*	Value of the quotient topology function. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) = (𝐽 qTop 𝐹))
Theorem	kqtopon 23663*	The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
Theorem	kqid 23664*	The topological indistinguishability map is a continuous function into the Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
Theorem	ist0-4 23665*	The topological indistinguishability map is injective iff the space is T0. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ 𝐹:𝑋–1-1→V))
Theorem	kqfvima 23666*	When the image set is open, the quotient map satisfies a partial converse to fnfvima 7224, which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑈 ↔ (𝐹‘𝐴) ∈ (𝐹 “ 𝑈)))
Theorem	kqsat 23667*	Any open set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 23653). (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈)
Theorem	kqdisj 23668*	A version of imain 6620 for the topological indistinguishability map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → ((𝐹 “ 𝑈) ∩ (𝐹 “ (𝐴 ∖ 𝑈))) = ∅)
Theorem	kqcldsat 23669*	Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 23653). (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈)
Theorem	kqopn 23670*	The topological indistinguishability map is an open map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (𝐹 “ 𝑈) ∈ (KQ‘𝐽))
Theorem	kqcld 23671*	The topological indistinguishability map is a closed map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑈) ∈ (Clsd‘(KQ‘𝐽)))
Theorem	kqt0lem 23672*	Lemma for kqt0 23682. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ Kol2)
Theorem	isr0 23673*	The property "𝐽 is an R0 space". A space is R0 if any two topologically distinguishable points are separated (there is an open set containing each one and disjoint from the other). Or in contraposition, if every open set which contains 𝑥 also contains 𝑦, so there is no separation, then 𝑥 and 𝑦 are members of the same open sets. We have chosen not to give this definition a name, because it turns out that a space is R0 if and only if its Kolmogorov quotient is T1, so that is what we prove here. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜))))
Theorem	r0cld 23674*	The analogue of the T1 axiom (singletons are closed) for an R0 space. In an R0 space the set of all points topologically indistinguishable from 𝐴 is closed. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴 ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜)} ∈ (Clsd‘𝐽))
Theorem	regr1lem 23675*	Lemma for regr1 23686. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Reg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → ¬ ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝐴) ∈ 𝑚 ∧ (𝐹‘𝐵) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑈 → 𝐵 ∈ 𝑈))
Theorem	regr1lem2 23676*	A Kolmogorov quotient of a regular space is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Haus)
Theorem	kqreglem1 23677*	A Kolmogorov quotient of a regular space is regular. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Reg)
Theorem	kqreglem2 23678*	If the Kolmogorov quotient of a space is regular then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Reg)
Theorem	kqnrmlem1 23679*	A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Nrm)
Theorem	kqnrmlem2 23680*	If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Nrm)
Theorem	kqtop 23681	The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Top ↔ (KQ‘𝐽) ∈ Top)
Theorem	kqt0 23682	The Kolmogorov quotient is T0 even if the original topology is not. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Top ↔ (KQ‘𝐽) ∈ Kol2)
Theorem	kqf 23683	The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ KQ:Top⟶Kol2
Theorem	r0sep 23684*	The separation property of an R0 space. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜)))
Theorem	nrmr0reg 23685	A normal R0 space is also regular. These spaces are usually referred to as normal regular spaces. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) → 𝐽 ∈ Reg)
Theorem	regr1 23686	A regular space is R1, which means that any two topologically distinct points can be separated by neighborhoods. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Reg → (KQ‘𝐽) ∈ Haus)
Theorem	kqreg 23687	The Kolmogorov quotient of a regular space is regular. By regr1 23686 it is also Hausdorff, so we can also say that a space is regular iff the Kolmogorov quotient is regular Hausdorff (T3). (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Reg ↔ (KQ‘𝐽) ∈ Reg)
Theorem	kqnrm 23688	The Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Nrm ↔ (KQ‘𝐽) ∈ Nrm)
12.1.21  Homeomorphisms
Syntax	chmeo 23689	Extend class notation with the class of all homeomorphisms.
class Homeo
Syntax	chmph 23690	Extend class notation with the relation "is homeomorphic to.".
class ≃
Definition	df-hmeo 23691*	Function returning all the homeomorphisms from topology 𝑗 to topology 𝑘. (Contributed by FL, 14-Feb-2007.)
⊢ Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)})
Definition	df-hmph 23692	Definition of the relation 𝑥 is homeomorphic to 𝑦. (Contributed by FL, 14-Feb-2007.)
⊢ ≃ = (◡Homeo “ (V ∖ 1o))
Theorem	hmeofn 23693	The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ Homeo Fn (Top × Top)
Theorem	hmeofval 23694*	The set of all the homeomorphisms between two topologies. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐽Homeo𝐾) = {𝑓 ∈ (𝐽 Cn 𝐾) ∣ ◡𝑓 ∈ (𝐾 Cn 𝐽)}
Theorem	ishmeo 23695	The predicate F is a homeomorphism between topology 𝐽 and topology 𝐾. Criterion of [BourbakiTop1] p. I.2. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ◡𝐹 ∈ (𝐾 Cn 𝐽)))
Theorem	hmeocn 23696	A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	hmeocnvcn 23697	The converse of a homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽))
Theorem	hmeocnv 23698	The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾Homeo𝐽))
Theorem	hmeof1o2 23699	A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽Homeo𝐾)) → 𝐹:𝑋–1-1-onto→𝑌)
Theorem	hmeof1o 23700	A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 30-May-2014.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→𝑌)