df-kq

Description: Define the Kolmogorov quotient. This is a function on topologies which maps a topology to its quotient under the topological distinguishability map, which takes a point to the set of open sets that contain it. Two points are mapped to the same image under this function iff they are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	df-kq	⊢ KQ = ( 𝑗 ∈ Top ↦ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ckq	⊢ KQ
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3	1	cv	⊢ 𝑗
4		cqtop	⊢ qTop
5		vx	⊢ 𝑥
6	3	cuni	⊢ ∪ 𝑗
7		vy	⊢ 𝑦
8	5	cv	⊢ 𝑥
9	7	cv	⊢ 𝑦
10	8 9	wcel	⊢ 𝑥 ∈ 𝑦
11	10 7 3	crab	⊢ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 }
12	5 6 11	cmpt	⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } )
13	3 12 4	co	⊢ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) )
14	1 2 13	cmpt	⊢ ( 𝑗 ∈ Top ↦ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) )
15	0 14	wceq	⊢ KQ = ( 𝑗 ∈ Top ↦ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) )

Metamath Proof Explorer

Definition df-kq

Detailed syntax breakdown