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 = { 𝑗 ∈ Top ∣ ∀ 𝑥 𝑗𝑦 𝑗 ( ∀ 𝑜𝑗 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ct0 Kol2
1 vj 𝑗
2 ctop Top
3 vx 𝑥
4 1 cv 𝑗
5 4 cuni 𝑗
6 vy 𝑦
7 vo 𝑜
8 3 cv 𝑥
9 7 cv 𝑜
10 8 9 wcel 𝑥𝑜
11 6 cv 𝑦
12 11 9 wcel 𝑦𝑜
13 10 12 wb ( 𝑥𝑜𝑦𝑜 )
14 13 7 4 wral 𝑜𝑗 ( 𝑥𝑜𝑦𝑜 )
15 8 11 wceq 𝑥 = 𝑦
16 14 15 wi ( ∀ 𝑜𝑗 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 )
17 16 6 5 wral 𝑦 𝑗 ( ∀ 𝑜𝑗 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 )
18 17 3 5 wral 𝑥 𝑗𝑦 𝑗 ( ∀ 𝑜𝑗 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 )
19 18 1 2 crab { 𝑗 ∈ Top ∣ ∀ 𝑥 𝑗𝑦 𝑗 ( ∀ 𝑜𝑗 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) }
20 0 19 wceq Kol2 = { 𝑗 ∈ Top ∣ ∀ 𝑥 𝑗𝑦 𝑗 ( ∀ 𝑜𝑗 ( 𝑥𝑜𝑦𝑜 ) → 𝑥 = 𝑦 ) }