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 ‘ 𝐽 ) 𝐴 = ( 𝑥 ∩ 𝑆 ) ) )