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