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 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
Assertion kqcld ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → F U ∈ Clsd ⁡ KQ ⁡ J

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
2 imassrn ⊢ F U ⊆ ran ⁡ F
3 2 a1i ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → F U ⊆ ran ⁡ F
4 1 kqcldsat ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → F -1 F U = U
5 simpr ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → U ∈ Clsd ⁡ J
6 4 5 eqeltrd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → F -1 F U ∈ Clsd ⁡ J
7 1 kqffn ⊢ J ∈ TopOn ⁡ X → F Fn X
8 dffn4 ⊢ F Fn X ↔ F : X ⟶ onto ran ⁡ F
9 7 8 sylib ⊢ J ∈ TopOn ⁡ X → F : X ⟶ onto ran ⁡ F
10 qtopcld ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto ran ⁡ F → F U ∈ Clsd ⁡ J qTop F ↔ F U ⊆ ran ⁡ F ∧ F -1 F U ∈ Clsd ⁡ J
11 9 10 mpdan ⊢ J ∈ TopOn ⁡ X → F U ∈ Clsd ⁡ J qTop F ↔ F U ⊆ ran ⁡ F ∧ F -1 F U ∈ Clsd ⁡ J
12 11 adantr ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → F U ∈ Clsd ⁡ J qTop F ↔ F U ⊆ ran ⁡ F ∧ F -1 F U ∈ Clsd ⁡ J
13 3 6 12 mpbir2and ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → F U ∈ Clsd ⁡ J qTop F
14 1 kqval ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J = J qTop F
15 14 adantr ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → KQ ⁡ J = J qTop F
16 15 fveq2d ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → Clsd ⁡ KQ ⁡ J = Clsd ⁡ J qTop F
17 13 16 eleqtrrd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ Clsd ⁡ J → F U ∈ Clsd ⁡ KQ ⁡ J