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 e. X |-> { y e. J | x e. y } )
Assertion kqopn 
|- ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( F " U ) e. ( KQ ` J ) )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 imassrn 
 |-  ( F " U ) C_ ran F
3 2 a1i 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( F " U ) C_ ran F )
4 1 kqsat 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( `' F " ( F " U ) ) = U )
5 simpr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> U e. J )
6 4 5 eqeltrd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( `' F " ( F " U ) ) e. J )
7 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
8 dffn4 
 |-  ( F Fn X <-> F : X -onto-> ran F )
9 7 8 sylib 
 |-  ( J e. ( TopOn ` X ) -> F : X -onto-> ran F )
10 9 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> F : X -onto-> ran F )
11 elqtop3 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ran F ) -> ( ( F " U ) e. ( J qTop F ) <-> ( ( F " U ) C_ ran F /\ ( `' F " ( F " U ) ) e. J ) ) )
12 10 11 syldan 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( ( F " U ) e. ( J qTop F ) <-> ( ( F " U ) C_ ran F /\ ( `' F " ( F " U ) ) e. J ) ) )
13 3 6 12 mpbir2and 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( F " U ) e. ( J qTop F ) )
14 1 kqval 
 |-  ( J e. ( TopOn ` X ) -> ( KQ ` J ) = ( J qTop F ) )
15 14 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( KQ ` J ) = ( J qTop F ) )
16 13 15 eleqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( F " U ) e. ( KQ ` J ) )