Theorem kqtop

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

	Ref	Expression
Assertion	kqtop	⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		toptopon2	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
2		eqid	⊢ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
3	2	kqtopon	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
4	1 3	sylbi	⊢ ( 𝐽 ∈ Top → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
5		topontop	⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) → ( KQ ‘ 𝐽 ) ∈ Top )
6	4 5	syl	⊢ ( 𝐽 ∈ Top → ( KQ ‘ 𝐽 ) ∈ Top )
7		0opn	⊢ ( ( KQ ‘ 𝐽 ) ∈ Top → ∅ ∈ ( KQ ‘ 𝐽 ) )
8		elfvdm	⊢ ( ∅ ∈ ( KQ ‘ 𝐽 ) → 𝐽 ∈ dom KQ )
9	7 8	syl	⊢ ( ( KQ ‘ 𝐽 ) ∈ Top → 𝐽 ∈ dom KQ )
10		ovex	⊢ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) ∈ V
11		df-kq	⊢ KQ = ( 𝑗 ∈ Top ↦ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) )
12	10 11	dmmpti	⊢ dom KQ = Top
13	9 12	eleqtrdi	⊢ ( ( KQ ‘ 𝐽 ) ∈ Top → 𝐽 ∈ Top )
14	6 13	impbii	⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Top )