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 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
Assertion kqopn ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F U ∈ 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 ∈ J → F U ⊆ ran ⁡ F
4 1 kqsat ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F -1 F U = U
5 simpr ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → U ∈ J
6 4 5 eqeltrd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F -1 F U ∈ 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 9 adantr ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F : X ⟶ onto ran ⁡ F
11 elqtop3 ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ onto ran ⁡ F → F U ∈ J qTop F ↔ F U ⊆ ran ⁡ F ∧ F -1 F U ∈ J
12 10 11 syldan ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F U ∈ J qTop F ↔ F U ⊆ ran ⁡ F ∧ F -1 F U ∈ J
13 3 6 12 mpbir2and ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F U ∈ J qTop F
14 1 kqval ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J = J qTop F
15 14 adantr ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → KQ ⁡ J = J qTop F
16 13 15 eleqtrrd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F U ∈ KQ ⁡ J