Metamath Proof Explorer


Theorem kqf

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

Proof

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