Metamath Proof Explorer

Definition df-t0

Description: Define T_0 or Kolmogorov spaces. A T_0 space satisfies a kind of "topological extensionality" principle (compare ax-ext ): any two points which are members of the same open sets are equal, or in contraposition, for any two distinct points there is an open set which contains one point but not the other. This differs from T_1 spaces (see ist1-2 ) in that in a T_1 space you can choose which point will be in the open set and which outside; in a T_0 space you only know that one of the two points is in the set. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion df-t0 ⊢ Kol2 = j ∈ Top | ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ct0 class Kol2
1 vj setvar j
2 ctop class Top
3 vx setvar x
4 1 cv setvar j
5 4 cuni class ⋃ j
6 vy setvar y
7 vo setvar o
8 3 cv setvar x
9 7 cv setvar o
10 8 9 wcel wff x ∈ o
11 6 cv setvar y
12 11 9 wcel wff y ∈ o
13 10 12 wb wff x ∈ o ↔ y ∈ o
14 13 7 4 wral wff ∀ o ∈ j x ∈ o ↔ y ∈ o
15 8 11 wceq wff x = y
16 14 15 wi wff ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y
17 16 6 5 wral wff ∀ y ∈ ⋃ j ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y
18 17 3 5 wral wff ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y
19 18 1 2 crab class j ∈ Top | ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y
20 0 19 wceq wff Kol2 = j ∈ Top | ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∀ o ∈ j x ∈ o ↔ y ∈ o → x = y