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 𝑋 = 𝐽
Assertion restcld ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ ( 𝐽t 𝑆 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( 𝑥𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 restcld.1 𝑋 = 𝐽
2 id ( 𝑆𝑋𝑆𝑋 )
3 1 topopn ( 𝐽 ∈ Top → 𝑋𝐽 )
4 ssexg ( ( 𝑆𝑋𝑋𝐽 ) → 𝑆 ∈ V )
5 2 3 4 syl2anr ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → 𝑆 ∈ V )
6 resttop ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝐽t 𝑆 ) ∈ Top )
7 5 6 syldan ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝐽t 𝑆 ) ∈ Top )
8 eqid ( 𝐽t 𝑆 ) = ( 𝐽t 𝑆 )
9 8 iscld ( ( 𝐽t 𝑆 ) ∈ Top → ( 𝐴 ∈ ( Clsd ‘ ( 𝐽t 𝑆 ) ) ↔ ( 𝐴 ( 𝐽t 𝑆 ) ∧ ( ( 𝐽t 𝑆 ) ∖ 𝐴 ) ∈ ( 𝐽t 𝑆 ) ) ) )
10 7 9 syl ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ ( 𝐽t 𝑆 ) ) ↔ ( 𝐴 ( 𝐽t 𝑆 ) ∧ ( ( 𝐽t 𝑆 ) ∖ 𝐴 ) ∈ ( 𝐽t 𝑆 ) ) ) )
11 1 restuni ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → 𝑆 = ( 𝐽t 𝑆 ) )
12 11 sseq2d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝐴𝑆𝐴 ( 𝐽t 𝑆 ) ) )
13 11 difeq1d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑆𝐴 ) = ( ( 𝐽t 𝑆 ) ∖ 𝐴 ) )
14 13 eleq1d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ↔ ( ( 𝐽t 𝑆 ) ∖ 𝐴 ) ∈ ( 𝐽t 𝑆 ) ) )
15 12 14 anbi12d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝐴𝑆 ∧ ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ) ↔ ( 𝐴 ( 𝐽t 𝑆 ) ∧ ( ( 𝐽t 𝑆 ) ∖ 𝐴 ) ∈ ( 𝐽t 𝑆 ) ) ) )
16 elrest ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ↔ ∃ 𝑜𝐽 ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) )
17 5 16 syldan ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ↔ ∃ 𝑜𝐽 ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) )
18 17 anbi2d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝐴𝑆 ∧ ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ) ↔ ( 𝐴𝑆 ∧ ∃ 𝑜𝐽 ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) ) )
19 1 opncld ( ( 𝐽 ∈ Top ∧ 𝑜𝐽 ) → ( 𝑋𝑜 ) ∈ ( Clsd ‘ 𝐽 ) )
20 19 ad5ant14 ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝐴𝑆 ) ∧ 𝑜𝐽 ) ∧ ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) → ( 𝑋𝑜 ) ∈ ( Clsd ‘ 𝐽 ) )
21 incom ( 𝑋𝑆 ) = ( 𝑆𝑋 )
22 df-ss ( 𝑆𝑋 ↔ ( 𝑆𝑋 ) = 𝑆 )
23 22 biimpi ( 𝑆𝑋 → ( 𝑆𝑋 ) = 𝑆 )
24 21 23 syl5eq ( 𝑆𝑋 → ( 𝑋𝑆 ) = 𝑆 )
25 24 ad4antlr ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝐴𝑆 ) ∧ 𝑜𝐽 ) ∧ ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) → ( 𝑋𝑆 ) = 𝑆 )
26 25 difeq1d ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝐴𝑆 ) ∧ 𝑜𝐽 ) ∧ ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) → ( ( 𝑋𝑆 ) ∖ 𝑜 ) = ( 𝑆𝑜 ) )
27 difeq2 ( ( 𝑆𝐴 ) = ( 𝑜𝑆 ) → ( 𝑆 ∖ ( 𝑆𝐴 ) ) = ( 𝑆 ∖ ( 𝑜𝑆 ) ) )
28 difindi ( 𝑆 ∖ ( 𝑜𝑆 ) ) = ( ( 𝑆𝑜 ) ∪ ( 𝑆𝑆 ) )
29 difid ( 𝑆𝑆 ) = ∅
30 29 uneq2i ( ( 𝑆𝑜 ) ∪ ( 𝑆𝑆 ) ) = ( ( 𝑆𝑜 ) ∪ ∅ )
31 un0 ( ( 𝑆𝑜 ) ∪ ∅ ) = ( 𝑆𝑜 )
32 28 30 31 3eqtri ( 𝑆 ∖ ( 𝑜𝑆 ) ) = ( 𝑆𝑜 )
33 27 32 eqtrdi ( ( 𝑆𝐴 ) = ( 𝑜𝑆 ) → ( 𝑆 ∖ ( 𝑆𝐴 ) ) = ( 𝑆𝑜 ) )
34 33 adantl ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝐴𝑆 ) ∧ 𝑜𝐽 ) ∧ ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) → ( 𝑆 ∖ ( 𝑆𝐴 ) ) = ( 𝑆𝑜 ) )
35 dfss4 ( 𝐴𝑆 ↔ ( 𝑆 ∖ ( 𝑆𝐴 ) ) = 𝐴 )
36 35 biimpi ( 𝐴𝑆 → ( 𝑆 ∖ ( 𝑆𝐴 ) ) = 𝐴 )
37 36 ad3antlr ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝐴𝑆 ) ∧ 𝑜𝐽 ) ∧ ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) → ( 𝑆 ∖ ( 𝑆𝐴 ) ) = 𝐴 )
38 26 34 37 3eqtr2rd ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝐴𝑆 ) ∧ 𝑜𝐽 ) ∧ ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) → 𝐴 = ( ( 𝑋𝑆 ) ∖ 𝑜 ) )
39 21 difeq1i ( ( 𝑋𝑆 ) ∖ 𝑜 ) = ( ( 𝑆𝑋 ) ∖ 𝑜 )
40 indif2 ( 𝑆 ∩ ( 𝑋𝑜 ) ) = ( ( 𝑆𝑋 ) ∖ 𝑜 )
41 incom ( 𝑆 ∩ ( 𝑋𝑜 ) ) = ( ( 𝑋𝑜 ) ∩ 𝑆 )
42 39 40 41 3eqtr2i ( ( 𝑋𝑆 ) ∖ 𝑜 ) = ( ( 𝑋𝑜 ) ∩ 𝑆 )
43 38 42 eqtrdi ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝐴𝑆 ) ∧ 𝑜𝐽 ) ∧ ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) → 𝐴 = ( ( 𝑋𝑜 ) ∩ 𝑆 ) )
44 ineq1 ( 𝑥 = ( 𝑋𝑜 ) → ( 𝑥𝑆 ) = ( ( 𝑋𝑜 ) ∩ 𝑆 ) )
45 44 rspceeqv ( ( ( 𝑋𝑜 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 = ( ( 𝑋𝑜 ) ∩ 𝑆 ) ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( 𝑥𝑆 ) )
46 20 43 45 syl2anc ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝐴𝑆 ) ∧ 𝑜𝐽 ) ∧ ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( 𝑥𝑆 ) )
47 46 rexlimdva2 ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝐴𝑆 ) → ( ∃ 𝑜𝐽 ( 𝑆𝐴 ) = ( 𝑜𝑆 ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( 𝑥𝑆 ) ) )
48 47 expimpd ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝐴𝑆 ∧ ∃ 𝑜𝐽 ( 𝑆𝐴 ) = ( 𝑜𝑆 ) ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( 𝑥𝑆 ) ) )
49 18 48 sylbid ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝐴𝑆 ∧ ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( 𝑥𝑆 ) ) )
50 difindi ( 𝑆 ∖ ( 𝑥𝑆 ) ) = ( ( 𝑆𝑥 ) ∪ ( 𝑆𝑆 ) )
51 29 uneq2i ( ( 𝑆𝑥 ) ∪ ( 𝑆𝑆 ) ) = ( ( 𝑆𝑥 ) ∪ ∅ )
52 un0 ( ( 𝑆𝑥 ) ∪ ∅ ) = ( 𝑆𝑥 )
53 50 51 52 3eqtri ( 𝑆 ∖ ( 𝑥𝑆 ) ) = ( 𝑆𝑥 )
54 difin2 ( 𝑆𝑋 → ( 𝑆𝑥 ) = ( ( 𝑋𝑥 ) ∩ 𝑆 ) )
55 54 adantl ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑆𝑥 ) = ( ( 𝑋𝑥 ) ∩ 𝑆 ) )
56 53 55 syl5eq ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑆 ∖ ( 𝑥𝑆 ) ) = ( ( 𝑋𝑥 ) ∩ 𝑆 ) )
57 56 adantr ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑆 ∖ ( 𝑥𝑆 ) ) = ( ( 𝑋𝑥 ) ∩ 𝑆 ) )
58 simpll ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐽 ∈ Top )
59 5 adantr ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑆 ∈ V )
60 1 cldopn ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋𝑥 ) ∈ 𝐽 )
61 60 adantl ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋𝑥 ) ∈ 𝐽 )
62 elrestr ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ∧ ( 𝑋𝑥 ) ∈ 𝐽 ) → ( ( 𝑋𝑥 ) ∩ 𝑆 ) ∈ ( 𝐽t 𝑆 ) )
63 58 59 61 62 syl3anc ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑋𝑥 ) ∩ 𝑆 ) ∈ ( 𝐽t 𝑆 ) )
64 57 63 eqeltrd ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑆 ∖ ( 𝑥𝑆 ) ) ∈ ( 𝐽t 𝑆 ) )
65 inss2 ( 𝑥𝑆 ) ⊆ 𝑆
66 64 65 jctil ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑥𝑆 ) ⊆ 𝑆 ∧ ( 𝑆 ∖ ( 𝑥𝑆 ) ) ∈ ( 𝐽t 𝑆 ) ) )
67 sseq1 ( 𝐴 = ( 𝑥𝑆 ) → ( 𝐴𝑆 ↔ ( 𝑥𝑆 ) ⊆ 𝑆 ) )
68 difeq2 ( 𝐴 = ( 𝑥𝑆 ) → ( 𝑆𝐴 ) = ( 𝑆 ∖ ( 𝑥𝑆 ) ) )
69 68 eleq1d ( 𝐴 = ( 𝑥𝑆 ) → ( ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ↔ ( 𝑆 ∖ ( 𝑥𝑆 ) ) ∈ ( 𝐽t 𝑆 ) ) )
70 67 69 anbi12d ( 𝐴 = ( 𝑥𝑆 ) → ( ( 𝐴𝑆 ∧ ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ) ↔ ( ( 𝑥𝑆 ) ⊆ 𝑆 ∧ ( 𝑆 ∖ ( 𝑥𝑆 ) ) ∈ ( 𝐽t 𝑆 ) ) ) )
71 66 70 syl5ibrcom ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 = ( 𝑥𝑆 ) → ( 𝐴𝑆 ∧ ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ) ) )
72 71 rexlimdva ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( 𝑥𝑆 ) → ( 𝐴𝑆 ∧ ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ) ) )
73 49 72 impbid ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( 𝐴𝑆 ∧ ( 𝑆𝐴 ) ∈ ( 𝐽t 𝑆 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( 𝑥𝑆 ) ) )
74 10 15 73 3bitr2d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝐴 ∈ ( Clsd ‘ ( 𝐽t 𝑆 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝐴 = ( 𝑥𝑆 ) ) )