Metamath Proof Explorer

Theorem ist0

Description: The predicate "is a T_0 space". Every pair of distinct points is topologically distinguishable. For the way this definition is usually encountered, see ist0-3 . (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Hypothesis ist0.1 ⊢X=⋃J
Assertion ist0 ⊢J∈Kol2↔J∈Top∧∀x∈X∀y∈X∀o∈Jx∈o↔y∈o→x=y

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢X=⋃J
2 unieq ⊢j=J→⋃j=⋃J
3 2 1 eqtr4di ⊢j=J→⋃j=X
4 raleq ⊢j=J→∀o∈jx∈o↔y∈o↔∀o∈Jx∈o↔y∈o
5 4 imbi1d ⊢j=J→∀o∈jx∈o↔y∈o→x=y↔∀o∈Jx∈o↔y∈o→x=y
6 3 5 raleqbidv ⊢j=J→∀y∈⋃j∀o∈jx∈o↔y∈o→x=y↔∀y∈X∀o∈Jx∈o↔y∈o→x=y
7 3 6 raleqbidv ⊢j=J→∀x∈⋃j∀y∈⋃j∀o∈jx∈o↔y∈o→x=y↔∀x∈X∀y∈X∀o∈Jx∈o↔y∈o→x=y
8 df-t0 ⊢Kol2=j∈Top|∀x∈⋃j∀y∈⋃j∀o∈jx∈o↔y∈o→x=y
9 7 8 elrab2 ⊢J∈Kol2↔J∈Top∧∀x∈X∀y∈X∀o∈Jx∈o↔y∈o→x=y