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 e. X |-> { y e. J | x e. y } )
Assertion kqcld 
|- ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( F " U ) e. ( Clsd ` ( 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. ( Clsd ` J ) ) -> ( F " U ) C_ ran F )
4 1 kqcldsat 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( `' F " ( F " U ) ) = U )
5 simpr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> U e. ( Clsd ` J ) )
6 4 5 eqeltrd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( `' F " ( F " U ) ) e. ( Clsd ` 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 qtopcld 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ran F ) -> ( ( F " U ) e. ( Clsd ` ( J qTop F ) ) <-> ( ( F " U ) C_ ran F /\ ( `' F " ( F " U ) ) e. ( Clsd ` J ) ) ) )
11 9 10 mpdan 
 |-  ( J e. ( TopOn ` X ) -> ( ( F " U ) e. ( Clsd ` ( J qTop F ) ) <-> ( ( F " U ) C_ ran F /\ ( `' F " ( F " U ) ) e. ( Clsd ` J ) ) ) )
12 11 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( ( F " U ) e. ( Clsd ` ( J qTop F ) ) <-> ( ( F " U ) C_ ran F /\ ( `' F " ( F " U ) ) e. ( Clsd ` J ) ) ) )
13 3 6 12 mpbir2and 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( F " U ) e. ( Clsd ` ( J qTop F ) ) )
14 1 kqval 
 |-  ( J e. ( TopOn ` X ) -> ( KQ ` J ) = ( J qTop F ) )
15 14 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( KQ ` J ) = ( J qTop F ) )
16 15 fveq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( Clsd ` ( KQ ` J ) ) = ( Clsd ` ( J qTop F ) ) )
17 13 16 eleqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( F " U ) e. ( Clsd ` ( KQ ` J ) ) )