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 ∈ J x ∈ 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 ∈ j x ∈ o ↔ y ∈ o ↔ ∀ o ∈ J x ∈ o ↔ y ∈ o
5 4 imbi1d ⊢ j = J → ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y ↔ ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
6 3 5 raleqbidv ⊢ j = J → ∀ y ∈ ⋃ j ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y ↔ ∀ y ∈ X ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
7 3 6 raleqbidv ⊢ j = J → ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y ↔ ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
8 df-t0 ⊢ Kol2 = j ∈ Top | ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y
9 7 8 elrab2 ⊢ J ∈ Kol2 ↔ J ∈ Top ∧ ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y