Metamath Proof Explorer

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 \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	kqid	$⊢ J \in TopOn (X) \to F \in (J Cn KQ (J))$

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
3		qtopid	$⊢ (J \in TopOn (X) \land F Fn X) \to F \in (J Cn (J qTop F))$
4	2 3	mpdan	$⊢ J \in TopOn (X) \to F \in (J Cn (J qTop F))$
5	1	kqval	$⊢ J \in TopOn (X) \to KQ (J) = J qTop F$
6	5	oveq2d	$⊢ J \in TopOn (X) \to J Cn KQ (J) = J Cn (J qTop F)$
7	4 6	eleqtrrd	$⊢ J \in TopOn (X) \to F \in (J Cn KQ (J))$