Metamath Proof Explorer

Theorem t1t0

Description: A T_1 space is a T_0 space. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion t1t0 ⊢J∈Fre→J∈Kol2

Proof

Step Hyp Ref Expression
1 t1top ⊢J∈Fre→J∈Top
2 toptopon2 ⊢J∈Top↔J∈TopOn⁡⋃J
3 1 2 sylib ⊢J∈Fre→J∈TopOn⁡⋃J
4 biimp ⊢x∈o↔y∈o→x∈o→y∈o
5 4 ralimi ⊢∀o∈Jx∈o↔y∈o→∀o∈Jx∈o→y∈o
6 5 imim1i ⊢∀o∈Jx∈o→y∈o→x=y→∀o∈Jx∈o↔y∈o→x=y
7 6 ralimi ⊢∀y∈⋃J∀o∈Jx∈o→y∈o→x=y→∀y∈⋃J∀o∈Jx∈o↔y∈o→x=y
8 7 ralimi ⊢∀x∈⋃J∀y∈⋃J∀o∈Jx∈o→y∈o→x=y→∀x∈⋃J∀y∈⋃J∀o∈Jx∈o↔y∈o→x=y
9 8 a1i ⊢J∈TopOn⁡⋃J→∀x∈⋃J∀y∈⋃J∀o∈Jx∈o→y∈o→x=y→∀x∈⋃J∀y∈⋃J∀o∈Jx∈o↔y∈o→x=y
10 ist1-2 ⊢J∈TopOn⁡⋃J→J∈Fre↔∀x∈⋃J∀y∈⋃J∀o∈Jx∈o→y∈o→x=y
11 ist0-2 ⊢J∈TopOn⁡⋃J→J∈Kol2↔∀x∈⋃J∀y∈⋃J∀o∈Jx∈o↔y∈o→x=y
12 9 10 11 3imtr4d ⊢J∈TopOn⁡⋃J→J∈Fre→J∈Kol2
13 3 12 mpcom ⊢J∈Fre→J∈Kol2