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

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2	1	kqval	$⊢ J \in TopOn (X) \to KQ (J) = J qTop F$
3	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
4		dffn4	$⊢ F Fn X \leftrightarrow F : X \underset{onto}{⟶} ran F$
5	3 4	sylib	$⊢ J \in TopOn (X) \to F : X \underset{onto}{⟶} ran F$
6		qtoptopon	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} ran F) \to J qTop F \in TopOn (ran F)$
7	5 6	mpdan	$⊢ J \in TopOn (X) \to J qTop F \in TopOn (ran F)$
8	2 7	eqeltrd	$⊢ J \in TopOn (X) \to KQ (J) \in TopOn (ran F)$

Metamath Proof Explorer