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	qtopuni 24001	The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹))
Theorem	elqtop3 24002	Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽)))
Theorem	qtoptopon 24003	The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
Theorem	qtopid 24004	A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
Theorem	idqtop 24005	The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 qTop ( I ↾ 𝑋)) = 𝐽)
Theorem	qtopcmplem 24006	Lemma for qtopcmp 24007 and qtopconn 24008. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top)    &   ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹:𝑋–onto→∪ (𝐽 qTop 𝐹) ∧ 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) → (𝐽 qTop 𝐹) ∈ 𝐴)    ⇒   ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ 𝐴)
Theorem	qtopcmp 24007	A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Comp)
Theorem	qtopconn 24008	A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Conn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Conn)
Theorem	qtopkgen 24009	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 24010	An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝐽 qTop 𝐹) ∈ TopBases)
Theorem	tgqtop 24011	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 24012	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 24013	Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾)))
Theorem	qtopss 24014	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 24004, 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 24015*	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 24016	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 24017*	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 24018*	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 24019	The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝑂 = (TopOpen‘𝑈)    ⇒   ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹))
Theorem	imastps 24020	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 24021	A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s 𝐸))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ TopSp)    ⇒   ⊢ (𝜑 → 𝑈 ∈ TopSp)
Theorem	kqfval 24022*	Value of the function appearing in df-kq 23993. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) = {𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦})
Theorem	kqfeq 24023*	Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐹‘𝐴) = (𝐹‘𝐵) ↔ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ↔ 𝐵 ∈ 𝑦)))
Theorem	kqffn 24024*	The topological indistinguishability map is a function on the base. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ 𝑉 → 𝐹 Fn 𝑋)
Theorem	kqval 24025*	Value of the quotient topology function. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) = (𝐽 qTop 𝐹))
Theorem	kqtopon 24026*	The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
Theorem	kqid 24027*	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 24028*	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 24029*	When the image set is open, the quotient map satisfies a partial converse to fnfvima 7231, which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑈 ↔ (𝐹‘𝐴) ∈ (𝐹 “ 𝑈)))
Theorem	kqsat 24030*	Any open set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 24016). (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈)
Theorem	kqdisj 24031*	A version of imain 6617 for the topological indistinguishability map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → ((𝐹 “ 𝑈) ∩ (𝐹 “ (𝐴 ∖ 𝑈))) = ∅)
Theorem	kqcldsat 24032*	Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 24016). (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈)
Theorem	kqopn 24033*	The topological indistinguishability map is an open map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (𝐹 “ 𝑈) ∈ (KQ‘𝐽))
Theorem	kqcld 24034*	The topological indistinguishability map is a closed map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑈) ∈ (Clsd‘(KQ‘𝐽)))
Theorem	kqt0lem 24035*	Lemma for kqt0 24045. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ Kol2)
Theorem	isr0 24036*	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 24037*	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 24038*	Lemma for regr1 24049. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Reg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → ¬ ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝐴) ∈ 𝑚 ∧ (𝐹‘𝐵) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑈 → 𝐵 ∈ 𝑈))
Theorem	regr1lem2 24039*	A Kolmogorov quotient of a regular space is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Haus)
Theorem	kqreglem1 24040*	A Kolmogorov quotient of a regular space is regular. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Reg)
Theorem	kqreglem2 24041*	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 24042*	A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Nrm)
Theorem	kqnrmlem2 24043*	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 24044	The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Top ↔ (KQ‘𝐽) ∈ Top)
Theorem	kqt0 24045	The Kolmogorov quotient is T0 even if the original topology is not. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Top ↔ (KQ‘𝐽) ∈ Kol2)
Theorem	kqf 24046	The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ KQ:Top⟶Kol2
Theorem	r0sep 24047*	The separation property of an R0 space. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜)))
Theorem	nrmr0reg 24048	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 24049	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 24050	The Kolmogorov quotient of a regular space is regular. By regr1 24049 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 24051	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 24052	Extend class notation with the class of all homeomorphisms.
class Homeo
Syntax	chmph 24053	Extend class notation with the relation "is homeomorphic to.".
class ≃
Definition	df-hmeo 24054*	Function returning all the homeomorphisms from topology 𝑗 to topology 𝑘. (Contributed by FL, 14-Feb-2007.)
⊢ Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)})
Definition	df-hmph 24055	Definition of the relation 𝑥 is homeomorphic to 𝑦. (Contributed by FL, 14-Feb-2007.)
⊢ ≃ = (◡Homeo “ (V ∖ 1o))
Theorem	hmeofn 24056	The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ Homeo Fn (Top × Top)
Theorem	hmeofval 24057*	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 24058	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 24059	A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	hmeocnvcn 24060	The converse of a homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽))
Theorem	hmeocnv 24061	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 24062	A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽Homeo𝐾)) → 𝐹:𝑋–1-1-onto→𝑌)
Theorem	hmeof1o 24063	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 24064	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 24065	Homeomorphisms preserve openness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐽 ↔ (𝐹 “ 𝐴) ∈ 𝐾))
Theorem	hmeocld 24066	Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘𝐽) ↔ (𝐹 “ 𝐴) ∈ (Clsd‘𝐾)))
Theorem	hmeocls 24067	Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐾)‘(𝐹 “ 𝐴)) = (𝐹 “ ((cls‘𝐽)‘𝐴)))
Theorem	hmeontr 24068	Homeomorphisms preserve interiors. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐾)‘(𝐹 “ 𝐴)) = (𝐹 “ ((int‘𝐽)‘𝐴)))
Theorem	hmeoimaf1o 24069*	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 24070	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 24071	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 24072	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 24073	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 24074	A homeomorphism is a quotient map. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐾 = (𝐽 qTop 𝐹))
Theorem	hmph 24075	Express the predicate 𝐽 is homeomorphic to 𝐾. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅)
Theorem	hmphi 24076	If there is a homeomorphism between spaces, then the spaces are homeomorphic. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐽 ≃ 𝐾)
Theorem	hmphtop 24077	Reverse closure for the homeomorphic predicate. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
Theorem	hmphtop1 24078	The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 → 𝐽 ∈ Top)
Theorem	hmphtop2 24079	The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 → 𝐾 ∈ Top)
Theorem	hmphref 24080	"Is homeomorphic to" is reflexive. (Contributed by FL, 25-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐽 ∈ Top → 𝐽 ≃ 𝐽)
Theorem	hmphsym 24081	"Is homeomorphic to" is symmetric. (Contributed by FL, 8-Mar-2007.) (Proof shortened by Mario Carneiro, 30-May-2014.)
⊢ (𝐽 ≃ 𝐾 → 𝐾 ≃ 𝐽)
Theorem	hmphtr 24082	"Is homeomorphic to" is transitive. (Contributed by FL, 9-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐽 ≃ 𝐾 ∧ 𝐾 ≃ 𝐿) → 𝐽 ≃ 𝐿)
Theorem	hmpher 24083	"Is homeomorphic to" is an equivalence relation. (Contributed by FL, 22-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ ≃ Er Top
Theorem	hmphen 24084	Homeomorphisms preserve the cardinality of the topologies. (Contributed by FL, 1-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐽 ≃ 𝐾 → 𝐽 ≈ 𝐾)
Theorem	hmphsymb 24085	"Is homeomorphic to" is symmetric. (Contributed by FL, 22-Feb-2007.)
⊢ (𝐽 ≃ 𝐾 ↔ 𝐾 ≃ 𝐽)
Theorem	haushmphlem 24086*	Lemma for haushmph 24091 and similar theorems. If the topological property 𝐴 is preserved under injective preimages, then property 𝐴 is preserved under homeomorphisms. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top)    &   ⊢ ((𝐽 ∈ 𝐴 ∧ 𝑓:∪ 𝐾–1-1→∪ 𝐽 ∧ 𝑓 ∈ (𝐾 Cn 𝐽)) → 𝐾 ∈ 𝐴)    ⇒   ⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴))
Theorem	cmphmph 24087	Compactness is a topological property-that is, for any two homeomorphic topologies, either both are compact or neither is. (Contributed by Jeff Hankins, 30-Jun-2009.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Comp → 𝐾 ∈ Comp))
Theorem	connhmph 24088	Connectedness is a topological property. (Contributed by Jeff Hankins, 3-Jul-2009.)
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Conn → 𝐾 ∈ Conn))
Theorem	t0hmph 24089	T0 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Kol2 → 𝐾 ∈ Kol2))
Theorem	t1hmph 24090	T1 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Fre → 𝐾 ∈ Fre))
Theorem	haushmph 24091	Hausdorff-ness is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Haus → 𝐾 ∈ Haus))
Theorem	reghmph 24092	Regularity is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Reg → 𝐾 ∈ Reg))
Theorem	nrmhmph 24093	Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
Theorem	hmph0 24094	A topology homeomorphic to the empty set is empty. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐽 ≃ {∅} ↔ 𝐽 = {∅})
Theorem	hmphdis 24095	Homeomorphisms preserve topological discreteness. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ≃ 𝒫 𝐴 → 𝐽 = 𝒫 𝑋)
Theorem	hmphindis 24096	Homeomorphisms preserve topological indiscreteness. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 = {∅, 𝑋})
Theorem	indishmph 24097	Equinumerous sets equipped with their indiscrete topologies are homeomorphic (which means in that particular case that a segment is homeomorphic to a circle contrary to what Wikipedia claims). (Contributed by FL, 17-Aug-2008.) (Proof shortened by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐴 ≈ 𝐵 → {∅, 𝐴} ≃ {∅, 𝐵})
Theorem	hmphen2 24098	Homeomorphisms preserve the cardinality of the underlying sets. (Contributed by FL, 17-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (𝐽 ≃ 𝐾 → 𝑋 ≈ 𝑌)
Theorem	cmphaushmeo 24099	A continuous bijection from a compact space to a Hausdorff space is a homeomorphism. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∈ (𝐽Homeo𝐾) ↔ 𝐹:𝑋–1-1-onto→𝑌))
Theorem	ordthmeolem 24100	Lemma for ordthmeo 24101. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝑌 = dom 𝑆    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆)))