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∈jx∈o↔y∈o→x=y

Detailed syntax breakdown

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