P. 241 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24001-24100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnmpt1res 24001*	The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.)
⊢ 𝐾 = (𝐽 ↾t 𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐿))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿))
Theorem	cnmpt2res 24002*	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 24003*	The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐾 ×t 𝐽) Cn 𝐿))
Theorem	cnmptkc 24004*	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 24005*	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 24006*	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 24007*	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 24008*	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 24009*	Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn 23981.) (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ 𝑋 = ∪ 𝑅    &   ⊢ 𝐹 = (𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))    ⇒   ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top) → 𝐹 ∈ (((𝑆 ↑ko 𝑅) ×t 𝑅) Cn 𝑆))
Theorem	cnmptk1p 24010*	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 24011*	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 24012*	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 24013*	The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
Theorem	txconn 24014	The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.)
⊢ ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Conn)
Theorem	imasnopn 24015	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 24016	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 24017	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 24018	Extend class notation with the Kolmogorov quotient function.
class KQ
Definition	df-kq 24019*	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 24020*	Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽})
Theorem	qtopval2 24021*	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 24022	Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽)))
Theorem	qtopres 24023	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 24024	The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐽 qTop 𝐹) ∈ Top)
Theorem	qtoptop 24025	The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
Theorem	elqtop2 24026	Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽)))
Theorem	qtopuni 24027	The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹))
Theorem	elqtop3 24028	Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽)))
Theorem	qtoptopon 24029	The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
Theorem	qtopid 24030	A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
Theorem	idqtop 24031	The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 qTop ( I ↾ 𝑋)) = 𝐽)
Theorem	qtopcmplem 24032	Lemma for qtopcmp 24033 and qtopconn 24034. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top)    &   ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹:𝑋–onto→∪ (𝐽 qTop 𝐹) ∧ 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) → (𝐽 qTop 𝐹) ∈ 𝐴)    ⇒   ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ 𝐴)
Theorem	qtopcmp 24033	A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Comp)
Theorem	qtopconn 24034	A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Conn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Conn)
Theorem	qtopkgen 24035	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 24036	An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝐽 qTop 𝐹) ∈ TopBases)
Theorem	tgqtop 24037	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 24038	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 24039	Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾)))
Theorem	qtopss 24040	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 24030, 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 24041*	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 24042	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 24043*	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 24044*	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 24045	The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝑂 = (TopOpen‘𝑈)    ⇒   ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹))
Theorem	imastps 24046	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 24047	A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s 𝐸))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ TopSp)    ⇒   ⊢ (𝜑 → 𝑈 ∈ TopSp)
Theorem	kqfval 24048*	Value of the function appearing in df-kq 24019. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) = {𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦})
Theorem	kqfeq 24049*	Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐹‘𝐴) = (𝐹‘𝐵) ↔ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ↔ 𝐵 ∈ 𝑦)))
Theorem	kqffn 24050*	The topological indistinguishability map is a function on the base. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ 𝑉 → 𝐹 Fn 𝑋)
Theorem	kqval 24051*	Value of the quotient topology function. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) = (𝐽 qTop 𝐹))
Theorem	kqtopon 24052*	The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
Theorem	kqid 24053*	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 24054*	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 24055*	When the image set is open, the quotient map satisfies a partial converse to fnfvima 7240, which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑈 ↔ (𝐹‘𝐴) ∈ (𝐹 “ 𝑈)))
Theorem	kqsat 24056*	Any open set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 24042). (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈)
Theorem	kqdisj 24057*	A version of imain 6626 for the topological indistinguishability map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → ((𝐹 “ 𝑈) ∩ (𝐹 “ (𝐴 ∖ 𝑈))) = ∅)
Theorem	kqcldsat 24058*	Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 24042). (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈)
Theorem	kqopn 24059*	The topological indistinguishability map is an open map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (𝐹 “ 𝑈) ∈ (KQ‘𝐽))
Theorem	kqcld 24060*	The topological indistinguishability map is a closed map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑈) ∈ (Clsd‘(KQ‘𝐽)))
Theorem	kqt0lem 24061*	Lemma for kqt0 24071. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ Kol2)
Theorem	isr0 24062*	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 24063*	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 24064*	Lemma for regr1 24075. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Reg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → ¬ ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝐴) ∈ 𝑚 ∧ (𝐹‘𝐵) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑈 → 𝐵 ∈ 𝑈))
Theorem	regr1lem2 24065*	A Kolmogorov quotient of a regular space is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Haus)
Theorem	kqreglem1 24066*	A Kolmogorov quotient of a regular space is regular. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Reg)
Theorem	kqreglem2 24067*	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 24068*	A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Nrm)
Theorem	kqnrmlem2 24069*	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 24070	The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Top ↔ (KQ‘𝐽) ∈ Top)
Theorem	kqt0 24071	The Kolmogorov quotient is T0 even if the original topology is not. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Top ↔ (KQ‘𝐽) ∈ Kol2)
Theorem	kqf 24072	The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ KQ:Top⟶Kol2
Theorem	r0sep 24073*	The separation property of an R0 space. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜)))
Theorem	nrmr0reg 24074	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 24075	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 24076	The Kolmogorov quotient of a regular space is regular. By regr1 24075 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 24077	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 24078	Extend class notation with the class of all homeomorphisms.
class Homeo
Syntax	chmph 24079	Extend class notation with the relation "is homeomorphic to.".
class ≃
Definition	df-hmeo 24080*	Function returning all the homeomorphisms from topology 𝑗 to topology 𝑘. (Contributed by FL, 14-Feb-2007.)
⊢ Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)})
Definition	df-hmph 24081	Definition of the relation 𝑥 is homeomorphic to 𝑦. (Contributed by FL, 14-Feb-2007.)
⊢ ≃ = (◡Homeo “ (V ∖ 1o))
Theorem	hmeofn 24082	The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ Homeo Fn (Top × Top)
Theorem	hmeofval 24083*	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 24084	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 24085	A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	hmeocnvcn 24086	The converse of a homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽))
Theorem	hmeocnv 24087	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 24088	A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽Homeo𝐾)) → 𝐹:𝑋–1-1-onto→𝑌)
Theorem	hmeof1o 24089	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→𝑌)
Theorem	hmeoima 24090	The image of an open set by a homeomorphism is an open set. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ∈ 𝐽) → (𝐹 “ 𝐴) ∈ 𝐾)
Theorem	hmeoopn 24091	Homeomorphisms preserve openness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐽 ↔ (𝐹 “ 𝐴) ∈ 𝐾))
Theorem	hmeocld 24092	Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘𝐽) ↔ (𝐹 “ 𝐴) ∈ (Clsd‘𝐾)))
Theorem	hmeocls 24093	Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐾)‘(𝐹 “ 𝐴)) = (𝐹 “ ((cls‘𝐽)‘𝐴)))
Theorem	hmeontr 24094	Homeomorphisms preserve interiors. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐾)‘(𝐹 “ 𝐴)) = (𝐹 “ ((int‘𝐽)‘𝐴)))
Theorem	hmeoimaf1o 24095*	The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐺 = (𝑥 ∈ 𝐽 ↦ (𝐹 “ 𝑥))    ⇒   ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐺:𝐽–1-1-onto→𝐾)
Theorem	hmeores 24096	The restriction of a homeomorphism is a homeomorphism. (Contributed by Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌))))
Theorem	hmeoco 24097	The composite of two homeomorphisms is a homeomorphism. (Contributed by FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐺 ∈ (𝐾Homeo𝐿)) → (𝐺 ∘ 𝐹) ∈ (𝐽Homeo𝐿))
Theorem	idhmeo 24098	The identity function is a homeomorphism. (Contributed by FL, 14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽Homeo𝐽))
Theorem	hmeocnvb 24099	The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ (Rel 𝐹 → (◡𝐹 ∈ (𝐽Homeo𝐾) ↔ 𝐹 ∈ (𝐾Homeo𝐽)))
Theorem	hmeoqtop 24100	A homeomorphism is a quotient map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐾 = (𝐽 qTop 𝐹))