Metamath Proof Explorer

Theorem kqcldsat

Description: Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest ). (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 
|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion kqcldsat 
|- ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( `' F " ( F " U ) ) = U )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
3 elpreima 
 |-  ( F Fn X -> ( z e. ( `' F " ( F " U ) ) <-> ( z e. X /\ ( F ` z ) e. ( F " U ) ) ) )
4 2 3 syl 
 |-  ( J e. ( TopOn ` X ) -> ( z e. ( `' F " ( F " U ) ) <-> ( z e. X /\ ( F ` z ) e. ( F " U ) ) ) )
5 4 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( z e. ( `' F " ( F " U ) ) <-> ( z e. X /\ ( F ` z ) e. ( F " U ) ) ) )
6 noel 
 |-  -. ( F ` z ) e. (/)
7 elin 
 |-  ( ( F ` z ) e. ( ( F " U ) i^i ( F " ( X \ U ) ) ) <-> ( ( F ` z ) e. ( F " U ) /\ ( F ` z ) e. ( F " ( X \ U ) ) ) )
8 incom 
 |-  ( ( F " U ) i^i ( F " ( X \ U ) ) ) = ( ( F " ( X \ U ) ) i^i ( F " U ) )
9 eqid 
 |-  U. J = U. J
10 9 cldss 
 |-  ( U e. ( Clsd ` J ) -> U C_ U. J )
11 10 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> U C_ U. J )
12 fndm 
 |-  ( F Fn X -> dom F = X )
13 2 12 syl 
 |-  ( J e. ( TopOn ` X ) -> dom F = X )
14 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
15 13 14 eqtrd 
 |-  ( J e. ( TopOn ` X ) -> dom F = U. J )
16 15 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> dom F = U. J )
17 11 16 sseqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> U C_ dom F )
18 13 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> dom F = X )
19 17 18 sseqtrd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> U C_ X )
20 19 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> U C_ X )
21 dfss4 
 |-  ( U C_ X <-> ( X \ ( X \ U ) ) = U )
22 20 21 sylib 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( X \ ( X \ U ) ) = U )
23 22 imaeq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( F " ( X \ ( X \ U ) ) ) = ( F " U ) )
24 23 ineq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( ( F " ( X \ U ) ) i^i ( F " ( X \ ( X \ U ) ) ) ) = ( ( F " ( X \ U ) ) i^i ( F " U ) ) )
25 simpll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> J e. ( TopOn ` X ) )
26 14 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> X = U. J )
27 26 difeq1d 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( X \ U ) = ( U. J \ U ) )
28 9 cldopn 
 |-  ( U e. ( Clsd ` J ) -> ( U. J \ U ) e. J )
29 28 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( U. J \ U ) e. J )
30 27 29 eqeltrd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( X \ U ) e. J )
31 30 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( X \ U ) e. J )
32 1 kqdisj 
 |-  ( ( J e. ( TopOn ` X ) /\ ( X \ U ) e. J ) -> ( ( F " ( X \ U ) ) i^i ( F " ( X \ ( X \ U ) ) ) ) = (/) )
33 25 31 32 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( ( F " ( X \ U ) ) i^i ( F " ( X \ ( X \ U ) ) ) ) = (/) )
34 24 33 eqtr3d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( ( F " ( X \ U ) ) i^i ( F " U ) ) = (/) )
35 8 34 syl5eq 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( ( F " U ) i^i ( F " ( X \ U ) ) ) = (/) )
36 35 eleq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( ( F ` z ) e. ( ( F " U ) i^i ( F " ( X \ U ) ) ) <-> ( F ` z ) e. (/) ) )
37 7 36 bitr3id 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( ( ( F ` z ) e. ( F " U ) /\ ( F ` z ) e. ( F " ( X \ U ) ) ) <-> ( F ` z ) e. (/) ) )
38 6 37 mtbiri 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> -. ( ( F ` z ) e. ( F " U ) /\ ( F ` z ) e. ( F " ( X \ U ) ) ) )
39 imnan 
 |-  ( ( ( F ` z ) e. ( F " U ) -> -. ( F ` z ) e. ( F " ( X \ U ) ) ) <-> -. ( ( F ` z ) e. ( F " U ) /\ ( F ` z ) e. ( F " ( X \ U ) ) ) )
40 38 39 sylibr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( ( F ` z ) e. ( F " U ) -> -. ( F ` z ) e. ( F " ( X \ U ) ) ) )
41 eldif 
 |-  ( z e. ( X \ U ) <-> ( z e. X /\ -. z e. U ) )
42 41 baibr 
 |-  ( z e. X -> ( -. z e. U <-> z e. ( X \ U ) ) )
43 42 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( -. z e. U <-> z e. ( X \ U ) ) )
44 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> z e. X )
45 1 kqfvima 
 |-  ( ( J e. ( TopOn ` X ) /\ ( X \ U ) e. J /\ z e. X ) -> ( z e. ( X \ U ) <-> ( F ` z ) e. ( F " ( X \ U ) ) ) )
46 25 31 44 45 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( z e. ( X \ U ) <-> ( F ` z ) e. ( F " ( X \ U ) ) ) )
47 43 46 bitrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( -. z e. U <-> ( F ` z ) e. ( F " ( X \ U ) ) ) )
48 47 con1bid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( -. ( F ` z ) e. ( F " ( X \ U ) ) <-> z e. U ) )
49 40 48 sylibd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) /\ z e. X ) -> ( ( F ` z ) e. ( F " U ) -> z e. U ) )
50 49 expimpd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( ( z e. X /\ ( F ` z ) e. ( F " U ) ) -> z e. U ) )
51 5 50 sylbid 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( z e. ( `' F " ( F " U ) ) -> z e. U ) )
52 51 ssrdv 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( `' F " ( F " U ) ) C_ U )
53 sseqin2 
 |-  ( U C_ dom F <-> ( dom F i^i U ) = U )
54 17 53 sylib 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( dom F i^i U ) = U )
55 dminss 
 |-  ( dom F i^i U ) C_ ( `' F " ( F " U ) )
56 54 55 eqsstrrdi 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> U C_ ( `' F " ( F " U ) ) )
57 52 56 eqssd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. ( Clsd ` J ) ) -> ( `' F " ( F " U ) ) = U )