Metamath Proof Explorer

Theorem ist0-2

Description: The predicate "is a T_0 space". (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion ist0-2 ⊢J∈TopOn⁡X→J∈Kol2↔∀x∈X∀y∈X∀o∈Jx∈o↔y∈o→x=y

Proof

Step Hyp Ref Expression
1 topontop ⊢J∈TopOn⁡X→J∈Top
2 eqid ⊢⋃J=⋃J
3 2 ist0 ⊢J∈Kol2↔J∈Top∧∀x∈⋃J∀y∈⋃J∀o∈Jx∈o↔y∈o→x=y
4 3 baib ⊢J∈Top→J∈Kol2↔∀x∈⋃J∀y∈⋃J∀o∈Jx∈o↔y∈o→x=y
5 1 4 syl ⊢J∈TopOn⁡X→J∈Kol2↔∀x∈⋃J∀y∈⋃J∀o∈Jx∈o↔y∈o→x=y
6 toponuni ⊢J∈TopOn⁡X→X=⋃J
7 6 raleqdv ⊢J∈TopOn⁡X→∀y∈X∀o∈Jx∈o↔y∈o→x=y↔∀y∈⋃J∀o∈Jx∈o↔y∈o→x=y
8 6 7 raleqbidv ⊢J∈TopOn⁡X→∀x∈X∀y∈X∀o∈Jx∈o↔y∈o→x=y↔∀x∈⋃J∀y∈⋃J∀o∈Jx∈o↔y∈o→x=y
9 5 8 bitr4d ⊢J∈TopOn⁡X→J∈Kol2↔∀x∈X∀y∈X∀o∈Jx∈o↔y∈o→x=y