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

Metamath Proof Explorer

Theorem kqopn

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

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

Proof

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