This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐽 ) ) )