Metamath Proof Explorer


Definition df-kq

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
Assertion df-kq
|- KQ = ( j e. Top |-> ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ckq
 |-  KQ
1 vj
 |-  j
2 ctop
 |-  Top
3 1 cv
 |-  j
4 cqtop
 |-  qTop
5 vx
 |-  x
6 3 cuni
 |-  U. j
7 vy
 |-  y
8 5 cv
 |-  x
9 7 cv
 |-  y
10 8 9 wcel
 |-  x e. y
11 10 7 3 crab
 |-  { y e. j | x e. y }
12 5 6 11 cmpt
 |-  ( x e. U. j |-> { y e. j | x e. y } )
13 3 12 4 co
 |-  ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) )
14 1 2 13 cmpt
 |-  ( j e. Top |-> ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) )
15 0 14 wceq
 |-  KQ = ( j e. Top |-> ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) )