Theorem kqcld

Description: The topological indistinguishability map is a closed map. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	kqval.2	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion	kqcld	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝑈 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		kqval.2	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2		imassrn	⊢ ( 𝐹 “ 𝑈 ) ⊆ ran 𝐹
3	2	a1i	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝑈 ) ⊆ ran 𝐹 )
4	1	kqcldsat	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) = 𝑈 )
5		simpr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ∈ ( Clsd ‘ 𝐽 ) )
6	4 5	eqeltrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ∈ ( Clsd ‘ 𝐽 ) )
7	1	kqffn	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
8		dffn4	⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
9	7 8	sylib	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 : 𝑋 –onto→ ran 𝐹 )
10		qtopcld	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ( ( 𝐹 “ 𝑈 ) ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝐹 “ 𝑈 ) ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
11	9 10	mpdan	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( 𝐹 “ 𝑈 ) ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝐹 “ 𝑈 ) ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
12	11	adantr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐹 “ 𝑈 ) ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝐹 “ 𝑈 ) ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
13	3 6 12	mpbir2and	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝑈 ) ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) )
14	1	kqval	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )
15	14	adantr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )
16	15	fveq2d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( Clsd ‘ ( KQ ‘ 𝐽 ) ) = ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) )
17	13 16	eleqtrrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝑈 ) ∈ ( Clsd ‘ ( KQ ‘ 𝐽 ) ) )