# 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}=\left({x}\in {X}⟼\left\{{y}\in {J}|{x}\in {y}\right\}\right)$
Assertion kqopn ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to {F}\left[{U}\right]\in \mathrm{KQ}\left({J}\right)$

### Proof

Step Hyp Ref Expression
1 kqval.2 ${⊢}{F}=\left({x}\in {X}⟼\left\{{y}\in {J}|{x}\in {y}\right\}\right)$
2 imassrn ${⊢}{F}\left[{U}\right]\subseteq \mathrm{ran}{F}$
3 2 a1i ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to {F}\left[{U}\right]\subseteq \mathrm{ran}{F}$
4 1 kqsat ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to {{F}}^{-1}\left[{F}\left[{U}\right]\right]={U}$
5 simpr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to {U}\in {J}$
6 4 5 eqeltrd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to {{F}}^{-1}\left[{F}\left[{U}\right]\right]\in {J}$
7 1 kqffn ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {F}Fn{X}$
8 dffn4 ${⊢}{F}Fn{X}↔{F}:{X}\underset{onto}{⟶}\mathrm{ran}{F}$
9 7 8 sylib ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {F}:{X}\underset{onto}{⟶}\mathrm{ran}{F}$
10 9 adantr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to {F}:{X}\underset{onto}{⟶}\mathrm{ran}{F}$
11 elqtop3 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}\mathrm{ran}{F}\right)\to \left({F}\left[{U}\right]\in \left({J}\mathrm{qTop}{F}\right)↔\left({F}\left[{U}\right]\subseteq \mathrm{ran}{F}\wedge {{F}}^{-1}\left[{F}\left[{U}\right]\right]\in {J}\right)\right)$
12 10 11 syldan ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to \left({F}\left[{U}\right]\in \left({J}\mathrm{qTop}{F}\right)↔\left({F}\left[{U}\right]\subseteq \mathrm{ran}{F}\wedge {{F}}^{-1}\left[{F}\left[{U}\right]\right]\in {J}\right)\right)$
13 3 6 12 mpbir2and ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to {F}\left[{U}\right]\in \left({J}\mathrm{qTop}{F}\right)$
14 1 kqval ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{KQ}\left({J}\right)={J}\mathrm{qTop}{F}$
15 14 adantr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to \mathrm{KQ}\left({J}\right)={J}\mathrm{qTop}{F}$
16 13 15 eleqtrrd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {U}\in {J}\right)\to {F}\left[{U}\right]\in \mathrm{KQ}\left({J}\right)$