Theorem kqf

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

	Ref	Expression
Assertion	kqf	$$⊢\mathrm{KQ}:\mathrm{Top}⟶\mathrm{Kol2}$$

Proof

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