P. 233 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23201-23300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnpf 23201	A continuous function at point 𝑃 is a mapping. (Contributed by FL, 17-Nov-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐹:𝑋⟶𝑌)
Theorem	cnpcl 23202	The value of a continuous function from 𝐽 to 𝐾 at point 𝑃 belongs to the underlying set of topology 𝐾. (Contributed by FL, 27-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ 𝑌)
Theorem	cnf2 23203	A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌)
Theorem	cnpf2 23204	A continuous function at point 𝑃 is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
Theorem	cnprcl2 23205	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑃 ∈ 𝑋)
Theorem	tgcn 23206*	The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 = (topGen‘𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)))
Theorem	tgcnp 23207*	The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 = (topGen‘𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
Theorem	subbascn 23208*	The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐾 = (topGen‘(fi‘𝐵)))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)))
Theorem	ssidcn 23209	The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (( I ↾ 𝑋) ∈ (𝐽 Cn 𝐾) ↔ 𝐾 ⊆ 𝐽))
Theorem	cnpimaex 23210*	Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.)
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝐴) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝐴))
Theorem	idcn 23211	A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽 Cn 𝐽))
Theorem	lmbr 23212*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a topological space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows to use objects more general than sequences when convenient; see the comment in df-lm 23183. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢))))
Theorem	lmbr2 23213*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))))
Theorem	lmbrf 23214*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmbr2 23213 presupposes that 𝐹 is a function. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢))))
Theorem	lmconst 23215	A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝑃})(⇝𝑡‘𝐽)𝑃)
Theorem	lmcvg 23216*	Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑈)
Theorem	iscnp4 23217*	The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃 " in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦)))
Theorem	cnpnei 23218*	A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
Theorem	cnima 23219	An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.)
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽)
Theorem	cnco 23220	The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐿)) → (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐿))
Theorem	cnpco 23221	The composition of a function 𝐹 continuous at 𝑃 with a function continuous at (𝐹‘𝑃) is continuous at 𝑃. Proposition 2 of [BourbakiTop1] p. I.9. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → (𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)‘𝑃))
Theorem	cnclima 23222	A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽))
Theorem	iscncl 23223*	A characterization of a continuity function using closed sets. Theorem 1(d) of [BourbakiTop1] p. I.9. (Contributed by FL, 19-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽))))
Theorem	cncls2i 23224	Property of the preimage of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐽)‘(◡𝐹 “ 𝑆)) ⊆ (◡𝐹 “ ((cls‘𝐾)‘𝑆)))
Theorem	cnntri 23225	Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑌) → (◡𝐹 “ ((int‘𝐾)‘𝑆)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑆)))
Theorem	cnclsi 23226	Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)))
Theorem	cncls2 23227*	Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑌((cls‘𝐽)‘(◡𝐹 “ 𝑥)) ⊆ (◡𝐹 “ ((cls‘𝐾)‘𝑥)))))
Theorem	cncls 23228*	Continuity in terms of closure. (Contributed by Jeff Hankins, 1-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑋(𝐹 “ ((cls‘𝐽)‘𝑥)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑥)))))
Theorem	cnntr 23229*	Continuity in terms of interior. (Contributed by Jeff Hankins, 2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑌(◡𝐹 “ ((int‘𝐾)‘𝑥)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑥)))))
Theorem	cnss1 23230	If the topology 𝐾 is finer than 𝐽, then there are more continuous functions from 𝐾 than from 𝐽. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝐽 Cn 𝐿) ⊆ (𝐾 Cn 𝐿))
Theorem	cnss2 23231	If the topology 𝐾 is finer than 𝐽, then there are fewer continuous functions into 𝐾 than into 𝐽 from some other space. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐿 ∈ (TopOn‘𝑌) ∧ 𝐿 ⊆ 𝐾) → (𝐽 Cn 𝐾) ⊆ (𝐽 Cn 𝐿))
Theorem	cncnpi 23232	A continuous function is continuous at all points. One direction of Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
Theorem	cnsscnp 23233	The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝑃 ∈ 𝑋 → (𝐽 Cn 𝐾) ⊆ ((𝐽 CnP 𝐾)‘𝑃))
Theorem	cncnp 23234*	A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
Theorem	cncnp2 23235*	A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (𝑋 ≠ ∅ → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))
Theorem	cnnei 23236*	Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑝 ∈ 𝑋 ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑝)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑝})(𝐹 “ 𝑣) ⊆ 𝑤))
Theorem	cnconst2 23237	A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ 𝑌) → (𝑋 × {𝐵}) ∈ (𝐽 Cn 𝐾))
Theorem	cnconst 23238	A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐵 ∈ 𝑌 ∧ 𝐹:𝑋⟶{𝐵})) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	cnrest 23239	Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾))
Theorem	cnrest2 23240	Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))))
Theorem	cnrest2r 23241	Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.)
⊢ (𝐾 ∈ Top → (𝐽 Cn (𝐾 ↾t 𝐵)) ⊆ (𝐽 Cn 𝐾))
Theorem	cnpresti 23242	One direction of cnprest 23243 under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 1-May-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑃 ∈ 𝐴 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃))
Theorem	cnprest 23243	Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃)))
Theorem	cnprest2 23244	Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ 𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃)))
Theorem	cndis 23245	Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝒫 𝐴 Cn 𝐽) = (𝑋 ↑m 𝐴))
Theorem	cnindis 23246	Every function is continuous when the codomain is indiscrete (trivial). (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 Cn {∅, 𝐴}) = (𝐴 ↑m 𝑋))
Theorem	cnpdis 23247	If 𝐴 is an isolated point in 𝑋 (or equivalently, the singleton {𝐴} is open in 𝑋), then every function is continuous at 𝐴. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → ((𝐽 CnP 𝐾)‘𝐴) = (𝑌 ↑m 𝑋))
Theorem	paste 23248	Pasting lemma. If 𝐴 and 𝐵 are closed sets in 𝑋 with 𝐴 ∪ 𝐵 = 𝑋, then any function whose restrictions to 𝐴 and 𝐵 are continuous is continuous on all of 𝑋. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝑋)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾))    &   ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ ((𝐽 ↾t 𝐵) Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	lmfpm 23249	If 𝐹 converges, then 𝐹 is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ∈ (𝑋 ↑pm ℂ))
Theorem	lmfss 23250	Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition). (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × 𝑋))
Theorem	lmcl 23251	Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ 𝑋)
Theorem	lmss 23252	Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ 𝐾 = (𝐽 ↾t 𝑌)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑌)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))
Theorem	sslm 23253	A finer topology has fewer convergent sequences (but the sequences that do converge, converge to the same value). (Contributed by Mario Carneiro, 15-Sep-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (⇝𝑡‘𝐾) ⊆ (⇝𝑡‘𝐽))
Theorem	lmres 23254	A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm ℂ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ↾ (ℤ≥‘𝑀))(⇝𝑡‘𝐽)𝑃))
Theorem	lmff 23255*	If 𝐹 converges, there is some upper integer set on which 𝐹 is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶𝑋)
Theorem	lmcls 23256*	Any convergent sequence of points in a subset of a topological space converges to a point in the closure of the subset. (Contributed by Mario Carneiro, 30-Dec-2013.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → 𝑃 ∈ ((cls‘𝐽)‘𝑆))
Theorem	lmcld 23257*	Any convergent sequence of points in a closed subset of a topological space converges to a point in the set. (Contributed by Mario Carneiro, 30-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝑆)
Theorem	lmcnp 23258	The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.)
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝑃))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹)(⇝𝑡‘𝐾)(𝐺‘𝑃))
Theorem	lmcn 23259	The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.)
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹)(⇝𝑡‘𝐾)(𝐺‘𝑃))
12.1.10  Separated spaces: T0, T1, T2 (Hausdorff) ...
Syntax	ct0 23260	Extend class notation with the class of all T0 spaces.
class Kol2
Syntax	ct1 23261	Extend class notation to include T1 spaces (also called Fréchet spaces).
class Fre
Syntax	cha 23262	Extend class notation with the class of all Hausdorff spaces.
class Haus
Syntax	creg 23263	Extend class notation with the class of all regular topologies.
class Reg
Syntax	cnrm 23264	Extend class notation with the class of all normal topologies.
class Nrm
Syntax	ccnrm 23265	Extend class notation with the class of all completely normal topologies.
class CNrm
Syntax	cpnrm 23266	Extend class notation with the class of all perfectly normal topologies.
class PNrm
Definition	df-t0 23267*	Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2706): any two points which are members of the same open sets are equal, or in contraposition, for any two distinct points there is an open set which contains one point but not the other. This differs from T1 spaces (see ist1-2 23301) in that in a T1 space you can choose which point will be in the open set and which outside; in a T0 space you only know that one of the two points is in the set. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ Kol2 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)}
Definition	df-t1 23268*	The class of all T1 spaces, also called Fréchet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007.)
⊢ Fre = {𝑥 ∈ Top ∣ ∀𝑎 ∈ ∪ 𝑥{𝑎} ∈ (Clsd‘𝑥)}
Definition	df-haus 23269*	Define the class of all Hausdorff (or T2) spaces. A Hausdorff space is a topology in which distinct points have disjoint open neighborhoods. Definition of Hausdorff space in [Munkres] p. 98. (Contributed by NM, 8-Mar-2007.)
⊢ Haus = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))}
Definition	df-reg 23270*	Define regular spaces. A space is regular if a point and a closed set can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ Reg = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑗 (𝑦 ∈ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
Definition	df-nrm 23271*	Define normal spaces. A space is normal if disjoint closed sets can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ ((Clsd‘𝑗) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝑗 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝑗)‘𝑧) ⊆ 𝑥)}
Definition	df-cnrm 23272*	Define completely normal spaces. A space is completely normal if all its subspaces are normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ CNrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 ∪ 𝑗(𝑗 ↾t 𝑥) ∈ Nrm}
Definition	df-pnrm 23273*	Define perfectly normal spaces. A space is perfectly normal if it is normal and every closed set is a Gδ set, meaning that it is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ PNrm = {𝑗 ∈ Nrm ∣ (Clsd‘𝑗) ⊆ ran (𝑓 ∈ (𝑗 ↑m ℕ) ↦ ∩ ran 𝑓)}
Theorem	ist0 23274*	The predicate "is a T0 space". Every pair of distinct points is topologically distinguishable. For the way this definition is usually encountered, see ist0-3 23299. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)))
Theorem	ist1 23275*	The predicate "is a T1 space". (Contributed by FL, 18-Jun-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Fre ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 {𝑎} ∈ (Clsd‘𝐽)))
Theorem	ishaus 23276*	The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
Theorem	iscnrm 23277*	The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ CNrm ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫 𝑋(𝐽 ↾t 𝑥) ∈ Nrm))
Theorem	t0sep 23278*	Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Kol2 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∀𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥) → 𝐴 = 𝐵))
Theorem	t0dist 23279*	Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Kol2 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵)) → ∃𝑜 ∈ 𝐽 ¬ (𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜))
Theorem	t1sncld 23280	In a T1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋) → {𝐴} ∈ (Clsd‘𝐽))
Theorem	t1ficld 23281	In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ (Clsd‘𝐽))
Theorem	hausnei 23282*	Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑃 ≠ 𝑄)) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	t0top 23283	A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Kol2 → 𝐽 ∈ Top)
Theorem	t1top 23284	A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Fre → 𝐽 ∈ Top)
Theorem	haustop 23285	A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.)
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
Theorem	isreg 23286*	The predicate "is a regular space". In a regular space, any open neighborhood has a closed subneighborhood. Note that some authors require the space to be Hausdorff (which would make it the same as T3), but we reserve the phrase "regular Hausdorff" for that as many topologists do. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐽 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
Theorem	regtop 23287	A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Reg → 𝐽 ∈ Top)
Theorem	regsep 23288*	In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ Reg ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ ((cls‘𝐽)‘𝑥) ⊆ 𝑈))
Theorem	isnrm 23289*	The predicate "is a normal space." Much like the case for regular spaces, normal does not imply Hausdorff or even regular. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐽 ∈ Nrm ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝐽 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ 𝑥)))
Theorem	nrmtop 23290	A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top)
Theorem	cnrmtop 23291	A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ CNrm → 𝐽 ∈ Top)
Theorem	iscnrm2 23292*	The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ CNrm ↔ ∀𝑥 ∈ 𝒫 𝑋(𝐽 ↾t 𝑥) ∈ Nrm))
Theorem	ispnrm 23293*	The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ PNrm ↔ (𝐽 ∈ Nrm ∧ (Clsd‘𝐽) ⊆ ran (𝑓 ∈ (𝐽 ↑m ℕ) ↦ ∩ ran 𝑓)))
Theorem	pnrmnrm 23294	A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ PNrm → 𝐽 ∈ Nrm)
Theorem	pnrmtop 23295	A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ PNrm → 𝐽 ∈ Top)
Theorem	pnrmcld 23296*	A closed set in a perfectly normal space is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐽 ∈ PNrm ∧ 𝐴 ∈ (Clsd‘𝐽)) → ∃𝑓 ∈ (𝐽 ↑m ℕ)𝐴 = ∩ ran 𝑓)
Theorem	pnrmopn 23297*	An open set in a perfectly normal space is a countable union of closed sets. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑m ℕ)𝐴 = ∪ ran 𝑓)
Theorem	ist0-2 23298*	The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)))
Theorem	ist0-3 23299*	The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑜 ∈ 𝐽 ((𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜) ∨ (¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜)))))
Theorem	cnt0 23300	The preimage of a T0 topology under an injective map is T0. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐾 ∈ Kol2 ∧ 𝐹:𝑋–1-1→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Kol2)