Definition df-t0 23361

Description: Define T₀ or Kolmogorov spaces. A T₀ space satisfies a kind of "topological extensionality" principle (compare ax-ext 2733): 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₁ spaces (see ist1-2 23395) in that in a T₁ space you can choose which point will be in the open set and which outside; in a T₀ space you only know that one of the two points is in the set. (Contributed by Jeff Hankins, 1-Feb-2010.)

Assertion

Ref	Expression
df-t0	⊢ Kol2 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)}

Distinct variable group:   𝑗,𝑜,𝑥,𝑦

Detailed syntax breakdown of Definition df-t0

Step	Hyp	Ref	Expression
1		ct0 23354	. 2 class Kol2
2		vx	. . . . . . . . 9 setvar 𝑥
3		vo	. . . . . . . . 9 setvar 𝑜
4	2, 3	wel 2142	. . . . . . . 8 wff 𝑥 ∈ 𝑜
5		vy	. . . . . . . . 9 setvar 𝑦
6	5, 3	wel 2142	. . . . . . . 8 wff 𝑦 ∈ 𝑜
7	4, 6	wb 208	. . . . . . 7 wff (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜)
8		vj	. . . . . . . 8 setvar 𝑗
9	8	cv 1558	. . . . . . 7 class 𝑗
10	7, 3, 9	wral 3075	. . . . . 6 wff ∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜)
11	2, 5	weq 1981	. . . . . 6 wff 𝑥 = 𝑦
12	10, 11	wi 4	. . . . 5 wff (∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)
13	9	cuni 4862	. . . . 5 class ∪ 𝑗
14	12, 5, 13	wral 3075	. . . 4 wff ∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)
15	14, 2, 13	wral 3075	. . 3 wff ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)
16		ctop 22941	. . 3 class Top
17	15, 8, 16	crab 3413	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)}
18	1, 17	wceq 1559	1 wff Kol2 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)}

This definition is referenced by:  ist0  23368