Metamath Proof Explorer

Theorem restcld

Description: A closed set of a subspace topology is a closed set of the original topology intersected with the subset. (Contributed by FL, 11-Jul-2009) (Proof shortened by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis restcld.1 
|- X = U. J
Assertion restcld 
|- ( ( J e. Top /\ S C_ X ) -> ( A e. ( Clsd ` ( J |`t S ) ) <-> E. x e. ( Clsd ` J ) A = ( x i^i S ) ) )

Proof

Step Hyp Ref Expression
1 restcld.1 
 |-  X = U. J
2 id 
 |-  ( S C_ X -> S C_ X )
3 1 topopn 
 |-  ( J e. Top -> X e. J )
4 ssexg 
 |-  ( ( S C_ X /\ X e. J ) -> S e. _V )
5 2 3 4 syl2anr 
 |-  ( ( J e. Top /\ S C_ X ) -> S e. _V )
6 resttop 
 |-  ( ( J e. Top /\ S e. _V ) -> ( J |`t S ) e. Top )
7 5 6 syldan 
 |-  ( ( J e. Top /\ S C_ X ) -> ( J |`t S ) e. Top )
8 eqid 
 |-  U. ( J |`t S ) = U. ( J |`t S )
9 8 iscld 
 |-  ( ( J |`t S ) e. Top -> ( A e. ( Clsd ` ( J |`t S ) ) <-> ( A C_ U. ( J |`t S ) /\ ( U. ( J |`t S ) \ A ) e. ( J |`t S ) ) ) )
10 7 9 syl 
 |-  ( ( J e. Top /\ S C_ X ) -> ( A e. ( Clsd ` ( J |`t S ) ) <-> ( A C_ U. ( J |`t S ) /\ ( U. ( J |`t S ) \ A ) e. ( J |`t S ) ) ) )
11 1 restuni 
 |-  ( ( J e. Top /\ S C_ X ) -> S = U. ( J |`t S ) )
12 11 sseq2d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( A C_ S <-> A C_ U. ( J |`t S ) ) )
13 11 difeq1d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( S \ A ) = ( U. ( J |`t S ) \ A ) )
14 13 eleq1d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( S \ A ) e. ( J |`t S ) <-> ( U. ( J |`t S ) \ A ) e. ( J |`t S ) ) )
15 12 14 anbi12d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( A C_ S /\ ( S \ A ) e. ( J |`t S ) ) <-> ( A C_ U. ( J |`t S ) /\ ( U. ( J |`t S ) \ A ) e. ( J |`t S ) ) ) )
16 elrest 
 |-  ( ( J e. Top /\ S e. _V ) -> ( ( S \ A ) e. ( J |`t S ) <-> E. o e. J ( S \ A ) = ( o i^i S ) ) )
17 5 16 syldan 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( S \ A ) e. ( J |`t S ) <-> E. o e. J ( S \ A ) = ( o i^i S ) ) )
18 17 anbi2d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( A C_ S /\ ( S \ A ) e. ( J |`t S ) ) <-> ( A C_ S /\ E. o e. J ( S \ A ) = ( o i^i S ) ) ) )
19 1 opncld 
 |-  ( ( J e. Top /\ o e. J ) -> ( X \ o ) e. ( Clsd ` J ) )
20 19 ad5ant14 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ A C_ S ) /\ o e. J ) /\ ( S \ A ) = ( o i^i S ) ) -> ( X \ o ) e. ( Clsd ` J ) )
21 incom 
 |-  ( X i^i S ) = ( S i^i X )
22 dfss2 
 |-  ( S C_ X <-> ( S i^i X ) = S )
23 22 biimpi 
 |-  ( S C_ X -> ( S i^i X ) = S )
24 21 23 eqtrid 
 |-  ( S C_ X -> ( X i^i S ) = S )
25 24 ad4antlr 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ A C_ S ) /\ o e. J ) /\ ( S \ A ) = ( o i^i S ) ) -> ( X i^i S ) = S )
26 25 difeq1d 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ A C_ S ) /\ o e. J ) /\ ( S \ A ) = ( o i^i S ) ) -> ( ( X i^i S ) \ o ) = ( S \ o ) )
27 difeq2 
 |-  ( ( S \ A ) = ( o i^i S ) -> ( S \ ( S \ A ) ) = ( S \ ( o i^i S ) ) )
28 difindi 
 |-  ( S \ ( o i^i S ) ) = ( ( S \ o ) u. ( S \ S ) )
29 difid 
 |-  ( S \ S ) = (/)
30 29 uneq2i 
 |-  ( ( S \ o ) u. ( S \ S ) ) = ( ( S \ o ) u. (/) )
31 un0 
 |-  ( ( S \ o ) u. (/) ) = ( S \ o )
32 28 30 31 3eqtri 
 |-  ( S \ ( o i^i S ) ) = ( S \ o )
33 27 32 eqtrdi 
 |-  ( ( S \ A ) = ( o i^i S ) -> ( S \ ( S \ A ) ) = ( S \ o ) )
34 33 adantl 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ A C_ S ) /\ o e. J ) /\ ( S \ A ) = ( o i^i S ) ) -> ( S \ ( S \ A ) ) = ( S \ o ) )
35 dfss4 
 |-  ( A C_ S <-> ( S \ ( S \ A ) ) = A )
36 35 biimpi 
 |-  ( A C_ S -> ( S \ ( S \ A ) ) = A )
37 36 ad3antlr 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ A C_ S ) /\ o e. J ) /\ ( S \ A ) = ( o i^i S ) ) -> ( S \ ( S \ A ) ) = A )
38 26 34 37 3eqtr2rd 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ A C_ S ) /\ o e. J ) /\ ( S \ A ) = ( o i^i S ) ) -> A = ( ( X i^i S ) \ o ) )
39 21 difeq1i 
 |-  ( ( X i^i S ) \ o ) = ( ( S i^i X ) \ o )
40 indif2 
 |-  ( S i^i ( X \ o ) ) = ( ( S i^i X ) \ o )
41 incom 
 |-  ( S i^i ( X \ o ) ) = ( ( X \ o ) i^i S )
42 39 40 41 3eqtr2i 
 |-  ( ( X i^i S ) \ o ) = ( ( X \ o ) i^i S )
43 38 42 eqtrdi 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ A C_ S ) /\ o e. J ) /\ ( S \ A ) = ( o i^i S ) ) -> A = ( ( X \ o ) i^i S ) )
44 ineq1 
 |-  ( x = ( X \ o ) -> ( x i^i S ) = ( ( X \ o ) i^i S ) )
45 44 rspceeqv 
 |-  ( ( ( X \ o ) e. ( Clsd ` J ) /\ A = ( ( X \ o ) i^i S ) ) -> E. x e. ( Clsd ` J ) A = ( x i^i S ) )
46 20 43 45 syl2anc 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ A C_ S ) /\ o e. J ) /\ ( S \ A ) = ( o i^i S ) ) -> E. x e. ( Clsd ` J ) A = ( x i^i S ) )
47 46 rexlimdva2 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ A C_ S ) -> ( E. o e. J ( S \ A ) = ( o i^i S ) -> E. x e. ( Clsd ` J ) A = ( x i^i S ) ) )
48 47 expimpd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( A C_ S /\ E. o e. J ( S \ A ) = ( o i^i S ) ) -> E. x e. ( Clsd ` J ) A = ( x i^i S ) ) )
49 18 48 sylbid 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( A C_ S /\ ( S \ A ) e. ( J |`t S ) ) -> E. x e. ( Clsd ` J ) A = ( x i^i S ) ) )
50 difindi 
 |-  ( S \ ( x i^i S ) ) = ( ( S \ x ) u. ( S \ S ) )
51 29 uneq2i 
 |-  ( ( S \ x ) u. ( S \ S ) ) = ( ( S \ x ) u. (/) )
52 un0 
 |-  ( ( S \ x ) u. (/) ) = ( S \ x )
53 50 51 52 3eqtri 
 |-  ( S \ ( x i^i S ) ) = ( S \ x )
54 difin2 
 |-  ( S C_ X -> ( S \ x ) = ( ( X \ x ) i^i S ) )
55 54 adantl 
 |-  ( ( J e. Top /\ S C_ X ) -> ( S \ x ) = ( ( X \ x ) i^i S ) )
56 53 55 eqtrid 
 |-  ( ( J e. Top /\ S C_ X ) -> ( S \ ( x i^i S ) ) = ( ( X \ x ) i^i S ) )
57 56 adantr 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( Clsd ` J ) ) -> ( S \ ( x i^i S ) ) = ( ( X \ x ) i^i S ) )
58 simpll 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( Clsd ` J ) ) -> J e. Top )
59 5 adantr 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( Clsd ` J ) ) -> S e. _V )
60 1 cldopn 
 |-  ( x e. ( Clsd ` J ) -> ( X \ x ) e. J )
61 60 adantl 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( Clsd ` J ) ) -> ( X \ x ) e. J )
62 elrestr 
 |-  ( ( J e. Top /\ S e. _V /\ ( X \ x ) e. J ) -> ( ( X \ x ) i^i S ) e. ( J |`t S ) )
63 58 59 61 62 syl3anc 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( Clsd ` J ) ) -> ( ( X \ x ) i^i S ) e. ( J |`t S ) )
64 57 63 eqeltrd 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( Clsd ` J ) ) -> ( S \ ( x i^i S ) ) e. ( J |`t S ) )
65 inss2 
 |-  ( x i^i S ) C_ S
66 64 65 jctil 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( Clsd ` J ) ) -> ( ( x i^i S ) C_ S /\ ( S \ ( x i^i S ) ) e. ( J |`t S ) ) )
67 sseq1 
 |-  ( A = ( x i^i S ) -> ( A C_ S <-> ( x i^i S ) C_ S ) )
68 difeq2 
 |-  ( A = ( x i^i S ) -> ( S \ A ) = ( S \ ( x i^i S ) ) )
69 68 eleq1d 
 |-  ( A = ( x i^i S ) -> ( ( S \ A ) e. ( J |`t S ) <-> ( S \ ( x i^i S ) ) e. ( J |`t S ) ) )
70 67 69 anbi12d 
 |-  ( A = ( x i^i S ) -> ( ( A C_ S /\ ( S \ A ) e. ( J |`t S ) ) <-> ( ( x i^i S ) C_ S /\ ( S \ ( x i^i S ) ) e. ( J |`t S ) ) ) )
71 66 70 syl5ibrcom 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( Clsd ` J ) ) -> ( A = ( x i^i S ) -> ( A C_ S /\ ( S \ A ) e. ( J |`t S ) ) ) )
72 71 rexlimdva 
 |-  ( ( J e. Top /\ S C_ X ) -> ( E. x e. ( Clsd ` J ) A = ( x i^i S ) -> ( A C_ S /\ ( S \ A ) e. ( J |`t S ) ) ) )
73 49 72 impbid 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( A C_ S /\ ( S \ A ) e. ( J |`t S ) ) <-> E. x e. ( Clsd ` J ) A = ( x i^i S ) ) )
74 10 15 73 3bitr2d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( A e. ( Clsd ` ( J |`t S ) ) <-> E. x e. ( Clsd ` J ) A = ( x i^i S ) ) )