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 ∈ J x ∈ 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 ∈ J x ∈ o ↔ y ∈ o → x = y
4 3 baib ⊢ J ∈ Top → J ∈ Kol2 ↔ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
5 1 4 syl ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
6 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
7 6 raleqdv ⊢ J ∈ TopOn ⁡ X → ∀ y ∈ X ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y ↔ ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
8 6 7 raleqbidv ⊢ J ∈ TopOn ⁡ X → ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y ↔ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
9 5 8 bitr4d ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y