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