Metamath Proof Explorer

Theorem restcls

Description: A closure in a subspace topology. (Contributed by Jeff Hankins, 22-Jan-2010) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypotheses restcls.1 
|- X = U. J
restcls.2 
|- K = ( J |`t Y )
Assertion restcls 
|- ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( cls ` K ) ` S ) = ( ( ( cls ` J ) ` S ) i^i Y ) )

Proof

Step Hyp Ref Expression
1 restcls.1 
 |-  X = U. J
2 restcls.2 
 |-  K = ( J |`t Y )
3 simp1 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> J e. Top )
4 sstr 
 |-  ( ( S C_ Y /\ Y C_ X ) -> S C_ X )
5 4 ancoms 
 |-  ( ( Y C_ X /\ S C_ Y ) -> S C_ X )
6 5 3adant1 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ X )
7 1 clscld 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
8 3 6 7 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
9 eqid 
 |-  ( ( ( cls ` J ) ` S ) i^i Y ) = ( ( ( cls ` J ) ` S ) i^i Y )
10 ineq1 
 |-  ( x = ( ( cls ` J ) ` S ) -> ( x i^i Y ) = ( ( ( cls ` J ) ` S ) i^i Y ) )
11 10 rspceeqv 
 |-  ( ( ( ( cls ` J ) ` S ) e. ( Clsd ` J ) /\ ( ( ( cls ` J ) ` S ) i^i Y ) = ( ( ( cls ` J ) ` S ) i^i Y ) ) -> E. x e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) i^i Y ) = ( x i^i Y ) )
12 8 9 11 sylancl 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> E. x e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) i^i Y ) = ( x i^i Y ) )
13 2 fveq2i 
 |-  ( Clsd ` K ) = ( Clsd ` ( J |`t Y ) )
14 13 eleq2i 
 |-  ( ( ( ( cls ` J ) ` S ) i^i Y ) e. ( Clsd ` K ) <-> ( ( ( cls ` J ) ` S ) i^i Y ) e. ( Clsd ` ( J |`t Y ) ) )
15 1 restcld 
 |-  ( ( J e. Top /\ Y C_ X ) -> ( ( ( ( cls ` J ) ` S ) i^i Y ) e. ( Clsd ` ( J |`t Y ) ) <-> E. x e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) i^i Y ) = ( x i^i Y ) ) )
16 15 3adant3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( ( cls ` J ) ` S ) i^i Y ) e. ( Clsd ` ( J |`t Y ) ) <-> E. x e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) i^i Y ) = ( x i^i Y ) ) )
17 14 16 syl5bb 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( ( cls ` J ) ` S ) i^i Y ) e. ( Clsd ` K ) <-> E. x e. ( Clsd ` J ) ( ( ( cls ` J ) ` S ) i^i Y ) = ( x i^i Y ) ) )
18 12 17 mpbird 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( cls ` J ) ` S ) i^i Y ) e. ( Clsd ` K ) )
19 1 sscls 
 |-  ( ( J e. Top /\ S C_ X ) -> S C_ ( ( cls ` J ) ` S ) )
20 3 6 19 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ ( ( cls ` J ) ` S ) )
21 simp3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ Y )
22 20 21 ssind 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ ( ( ( cls ` J ) ` S ) i^i Y ) )
23 eqid 
 |-  U. K = U. K
24 23 clsss2 
 |-  ( ( ( ( ( cls ` J ) ` S ) i^i Y ) e. ( Clsd ` K ) /\ S C_ ( ( ( cls ` J ) ` S ) i^i Y ) ) -> ( ( cls ` K ) ` S ) C_ ( ( ( cls ` J ) ` S ) i^i Y ) )
25 18 22 24 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( cls ` K ) ` S ) C_ ( ( ( cls ` J ) ` S ) i^i Y ) )
26 2 fveq2i 
 |-  ( cls ` K ) = ( cls ` ( J |`t Y ) )
27 26 fveq1i 
 |-  ( ( cls ` K ) ` S ) = ( ( cls ` ( J |`t Y ) ) ` S )
28 id 
 |-  ( Y C_ X -> Y C_ X )
29 1 topopn 
 |-  ( J e. Top -> X e. J )
30 ssexg 
 |-  ( ( Y C_ X /\ X e. J ) -> Y e. _V )
31 28 29 30 syl2anr 
 |-  ( ( J e. Top /\ Y C_ X ) -> Y e. _V )
32 resttop 
 |-  ( ( J e. Top /\ Y e. _V ) -> ( J |`t Y ) e. Top )
33 31 32 syldan 
 |-  ( ( J e. Top /\ Y C_ X ) -> ( J |`t Y ) e. Top )
34 33 3adant3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( J |`t Y ) e. Top )
35 1 restuni 
 |-  ( ( J e. Top /\ Y C_ X ) -> Y = U. ( J |`t Y ) )
36 35 3adant3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> Y = U. ( J |`t Y ) )
37 21 36 sseqtrd 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ U. ( J |`t Y ) )
38 eqid 
 |-  U. ( J |`t Y ) = U. ( J |`t Y )
39 38 clscld 
 |-  ( ( ( J |`t Y ) e. Top /\ S C_ U. ( J |`t Y ) ) -> ( ( cls ` ( J |`t Y ) ) ` S ) e. ( Clsd ` ( J |`t Y ) ) )
40 34 37 39 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( cls ` ( J |`t Y ) ) ` S ) e. ( Clsd ` ( J |`t Y ) ) )
41 27 40 eqeltrid 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( cls ` K ) ` S ) e. ( Clsd ` ( J |`t Y ) ) )
42 1 restcld 
 |-  ( ( J e. Top /\ Y C_ X ) -> ( ( ( cls ` K ) ` S ) e. ( Clsd ` ( J |`t Y ) ) <-> E. x e. ( Clsd ` J ) ( ( cls ` K ) ` S ) = ( x i^i Y ) ) )
43 42 3adant3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( cls ` K ) ` S ) e. ( Clsd ` ( J |`t Y ) ) <-> E. x e. ( Clsd ` J ) ( ( cls ` K ) ` S ) = ( x i^i Y ) ) )
44 41 43 mpbid 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> E. x e. ( Clsd ` J ) ( ( cls ` K ) ` S ) = ( x i^i Y ) )
45 2 33 eqeltrid 
 |-  ( ( J e. Top /\ Y C_ X ) -> K e. Top )
46 45 3adant3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> K e. Top )
47 2 unieqi 
 |-  U. K = U. ( J |`t Y )
48 47 eqcomi 
 |-  U. ( J |`t Y ) = U. K
49 48 sscls 
 |-  ( ( K e. Top /\ S C_ U. ( J |`t Y ) ) -> S C_ ( ( cls ` K ) ` S ) )
50 46 37 49 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ ( ( cls ` K ) ` S ) )
51 50 adantr 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( x e. ( Clsd ` J ) /\ ( ( cls ` K ) ` S ) = ( x i^i Y ) ) ) -> S C_ ( ( cls ` K ) ` S ) )
52 inss1 
 |-  ( x i^i Y ) C_ x
53 sseq1 
 |-  ( ( ( cls ` K ) ` S ) = ( x i^i Y ) -> ( ( ( cls ` K ) ` S ) C_ x <-> ( x i^i Y ) C_ x ) )
54 52 53 mpbiri 
 |-  ( ( ( cls ` K ) ` S ) = ( x i^i Y ) -> ( ( cls ` K ) ` S ) C_ x )
55 54 ad2antll 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( x e. ( Clsd ` J ) /\ ( ( cls ` K ) ` S ) = ( x i^i Y ) ) ) -> ( ( cls ` K ) ` S ) C_ x )
56 51 55 sstrd 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( x e. ( Clsd ` J ) /\ ( ( cls ` K ) ` S ) = ( x i^i Y ) ) ) -> S C_ x )
57 1 clsss2 
 |-  ( ( x e. ( Clsd ` J ) /\ S C_ x ) -> ( ( cls ` J ) ` S ) C_ x )
58 57 adantl 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( x e. ( Clsd ` J ) /\ S C_ x ) ) -> ( ( cls ` J ) ` S ) C_ x )
59 58 ssrind 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( x e. ( Clsd ` J ) /\ S C_ x ) ) -> ( ( ( cls ` J ) ` S ) i^i Y ) C_ ( x i^i Y ) )
60 sseq2 
 |-  ( ( ( cls ` K ) ` S ) = ( x i^i Y ) -> ( ( ( ( cls ` J ) ` S ) i^i Y ) C_ ( ( cls ` K ) ` S ) <-> ( ( ( cls ` J ) ` S ) i^i Y ) C_ ( x i^i Y ) ) )
61 59 60 syl5ibrcom 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( x e. ( Clsd ` J ) /\ S C_ x ) ) -> ( ( ( cls ` K ) ` S ) = ( x i^i Y ) -> ( ( ( cls ` J ) ` S ) i^i Y ) C_ ( ( cls ` K ) ` S ) ) )
62 61 expr 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ x e. ( Clsd ` J ) ) -> ( S C_ x -> ( ( ( cls ` K ) ` S ) = ( x i^i Y ) -> ( ( ( cls ` J ) ` S ) i^i Y ) C_ ( ( cls ` K ) ` S ) ) ) )
63 62 com23 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ x e. ( Clsd ` J ) ) -> ( ( ( cls ` K ) ` S ) = ( x i^i Y ) -> ( S C_ x -> ( ( ( cls ` J ) ` S ) i^i Y ) C_ ( ( cls ` K ) ` S ) ) ) )
64 63 impr 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( x e. ( Clsd ` J ) /\ ( ( cls ` K ) ` S ) = ( x i^i Y ) ) ) -> ( S C_ x -> ( ( ( cls ` J ) ` S ) i^i Y ) C_ ( ( cls ` K ) ` S ) ) )
65 56 64 mpd 
 |-  ( ( ( J e. Top /\ Y C_ X /\ S C_ Y ) /\ ( x e. ( Clsd ` J ) /\ ( ( cls ` K ) ` S ) = ( x i^i Y ) ) ) -> ( ( ( cls ` J ) ` S ) i^i Y ) C_ ( ( cls ` K ) ` S ) )
66 44 65 rexlimddv 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( ( cls ` J ) ` S ) i^i Y ) C_ ( ( cls ` K ) ` S ) )
67 25 66 eqssd 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( cls ` K ) ` S ) = ( ( ( cls ` J ) ` S ) i^i Y ) )