Theorem kqid

Description: The topological indistinguishability map is a continuous function into the Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		kqval.2	|- F = ( x e. X |-> { y e. J | x e. y } )
2	1	kqffn	|- ( J e. ( TopOn ` X ) -> F Fn X )
3		qtopid	|- ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
4	2 3	mpdan	|- ( J e. ( TopOn ` X ) -> F e. ( J Cn ( J qTop F ) ) )
5	1	kqval	|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) = ( J qTop F ) )
6	5	oveq2d	|- ( J e. ( TopOn ` X ) -> ( J Cn ( KQ ` J ) ) = ( J Cn ( J qTop F ) ) )
7	4 6	eleqtrrd	|- ( J e. ( TopOn ` X ) -> F e. ( J Cn ( KQ ` J ) ) )