![]() |
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 23717 | . 2 class KQ | |
2 | vj | . . 3 setvar 𝑗 | |
3 | ctop 22915 | . . 3 class Top | |
4 | 2 | cv 1536 | . . . 4 class 𝑗 |
5 | vx | . . . . 5 setvar 𝑥 | |
6 | 4 | cuni 4912 | . . . . 5 class ∪ 𝑗 |
7 | vy | . . . . . . 7 setvar 𝑦 | |
8 | 5, 7 | wel 2107 | . . . . . 6 wff 𝑥 ∈ 𝑦 |
9 | 8, 7, 4 | crab 3433 | . . . . 5 class {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦} |
10 | 5, 6, 9 | cmpt 5231 | . . . 4 class (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦}) |
11 | cqtop 17550 | . . . 4 class qTop | |
12 | 4, 10, 11 | co 7431 | . . 3 class (𝑗 qTop (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦})) |
13 | 2, 3, 12 | cmpt 5231 | . 2 class (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦}))) |
14 | 1, 13 | wceq 1537 | 1 wff KQ = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦}))) |
Colors of variables: wff setvar class |
This definition is referenced by: kqval 23750 kqtop 23769 kqf 23771 |
Copyright terms: Public domain | W3C validator |