Theorem 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

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) ∈ V
2		df-kq	⊢ KQ = ( 𝑗 ∈ Top ↦ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) )
3	1 2	fnmpti	⊢ KQ Fn Top
4		kqt0	⊢ ( 𝑥 ∈ Top ↔ ( KQ ‘ 𝑥 ) ∈ Kol2 )
5	4	biimpi	⊢ ( 𝑥 ∈ Top → ( KQ ‘ 𝑥 ) ∈ Kol2 )
6	5	rgen	⊢ ∀ 𝑥 ∈ Top ( KQ ‘ 𝑥 ) ∈ Kol2
7		ffnfv	⊢ ( KQ : Top ⟶ Kol2 ↔ ( KQ Fn Top ∧ ∀ 𝑥 ∈ Top ( KQ ‘ 𝑥 ) ∈ Kol2 ) )
8	3 6 7	mpbir2an	⊢ KQ : Top ⟶ Kol2