| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-t0 | Structured version Visualization version GIF version | ||
| Description: Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2708): 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 T1 spaces (see ist1-2 23355) in that in a T1 space you can choose which point will be in the open set and which outside; in a T0 space you only know that one of the two points is in the set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
| Ref | Expression |
|---|---|
| df-t0 | ⊢ Kol2 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ct0 23314 | . 2 class Kol2 | |
| 2 | vx | . . . . . . . . 9 setvar 𝑥 | |
| 3 | vo | . . . . . . . . 9 setvar 𝑜 | |
| 4 | 2, 3 | wel 2109 | . . . . . . . 8 wff 𝑥 ∈ 𝑜 |
| 5 | vy | . . . . . . . . 9 setvar 𝑦 | |
| 6 | 5, 3 | wel 2109 | . . . . . . . 8 wff 𝑦 ∈ 𝑜 |
| 7 | 4, 6 | wb 206 | . . . . . . 7 wff (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) |
| 8 | vj | . . . . . . . 8 setvar 𝑗 | |
| 9 | 8 | cv 1539 | . . . . . . 7 class 𝑗 |
| 10 | 7, 3, 9 | wral 3061 | . . . . . 6 wff ∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) |
| 11 | 2, 5 | weq 1962 | . . . . . 6 wff 𝑥 = 𝑦 |
| 12 | 10, 11 | wi 4 | . . . . 5 wff (∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦) |
| 13 | 9 | cuni 4907 | . . . . 5 class ∪ 𝑗 |
| 14 | 12, 5, 13 | wral 3061 | . . . 4 wff ∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦) |
| 15 | 14, 2, 13 | wral 3061 | . . 3 wff ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦) |
| 16 | ctop 22899 | . . 3 class Top | |
| 17 | 15, 8, 16 | crab 3436 | . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)} |
| 18 | 1, 17 | wceq 1540 | 1 wff Kol2 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(∀𝑜 ∈ 𝑗 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)} |
| Colors of variables: wff setvar class |
| This definition is referenced by: ist0 23328 |
| Copyright terms: Public domain | W3C validator |