|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > df-kq | Structured version Visualization version GIF version | ||
| Description: Define the Kolmogorov quotient. This is a function on topologies which maps a topology to its quotient under the topological distinguishability map, which takes a point to the set of open sets that contain it. Two points are mapped to the same image under this function iff they are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.) | 
| Ref | Expression | 
|---|---|
| df-kq | ⊢ KQ = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦}))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ckq 23702 | . 2 class KQ | |
| 2 | vj | . . 3 setvar 𝑗 | |
| 3 | ctop 22900 | . . 3 class Top | |
| 4 | 2 | cv 1538 | . . . 4 class 𝑗 | 
| 5 | vx | . . . . 5 setvar 𝑥 | |
| 6 | 4 | cuni 4906 | . . . . 5 class ∪ 𝑗 | 
| 7 | vy | . . . . . . 7 setvar 𝑦 | |
| 8 | 5, 7 | wel 2108 | . . . . . 6 wff 𝑥 ∈ 𝑦 | 
| 9 | 8, 7, 4 | crab 3435 | . . . . 5 class {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦} | 
| 10 | 5, 6, 9 | cmpt 5224 | . . . 4 class (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦}) | 
| 11 | cqtop 17549 | . . . 4 class qTop | |
| 12 | 4, 10, 11 | co 7432 | . . 3 class (𝑗 qTop (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦})) | 
| 13 | 2, 3, 12 | cmpt 5224 | . 2 class (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦}))) | 
| 14 | 1, 13 | wceq 1539 | 1 wff KQ = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦}))) | 
| Colors of variables: wff setvar class | 
| This definition is referenced by: kqval 23735 kqtop 23754 kqf 23756 | 
| Copyright terms: Public domain | W3C validator |