Theorem kqtopon

Description: The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	kqval.2	|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion	kqtopon	|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )

Proof

Step	Hyp	Ref	Expression
1		kqval.2	|- F = ( x e. X |-> { y e. J | x e. y } )
2	1	kqval	|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) = ( J qTop F ) )
3	1	kqffn	|- ( J e. ( TopOn ` X ) -> F Fn X )
4		dffn4	|- ( F Fn X <-> F : X -onto-> ran F )
5	3 4	sylib	|- ( J e. ( TopOn ` X ) -> F : X -onto-> ran F )
6		qtoptopon	|- ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ran F ) -> ( J qTop F ) e. ( TopOn ` ran F ) )
7	5 6	mpdan	|- ( J e. ( TopOn ` X ) -> ( J qTop F ) e. ( TopOn ` ran F ) )
8	2 7	eqeltrd	|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )