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$

Step	Hyp	Ref	Expression
1		ovex	$⊢ j qTop (x \in ⋃ j ⟼ \{y \in j \| x \in y\}) \in V$
2		df-kq	$⊢ KQ = (j \in Top ⟼ j qTop (x \in ⋃ j ⟼ \{y \in j \| x \in y\}))$
3	1 2	fnmpti	$⊢ KQ Fn Top$
4		kqt0	$⊢ x \in Top \leftrightarrow KQ (x) \in Kol2$
5	4	biimpi	$⊢ x \in Top \to KQ (x) \in Kol2$
6	5	rgen	$⊢ \forall x \in Top KQ (x) \in Kol2$
7		ffnfv	$⊢ KQ : Top ⟶ Kol2 \leftrightarrow (KQ Fn Top \land \forall x \in Top KQ (x) \in Kol2)$
8	3 6 7	mpbir2an	$⊢ KQ : Top ⟶ Kol2$

Metamath Proof Explorer