Description: The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | kqf | |- KQ : Top --> Kol2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovex | |- ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) e. _V |
|
2 | df-kq | |- KQ = ( j e. Top |-> ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) ) |
|
3 | 1 2 | fnmpti | |- KQ Fn Top |
4 | kqt0 | |- ( x e. Top <-> ( KQ ` x ) e. Kol2 ) |
|
5 | 4 | biimpi | |- ( x e. Top -> ( KQ ` x ) e. Kol2 ) |
6 | 5 | rgen | |- A. x e. Top ( KQ ` x ) e. Kol2 |
7 | ffnfv | |- ( KQ : Top --> Kol2 <-> ( KQ Fn Top /\ A. x e. Top ( KQ ` x ) e. Kol2 ) ) |
|
8 | 3 6 7 | mpbir2an | |- KQ : Top --> Kol2 |