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 = J
Assertion restcld J Top S X A Clsd J 𝑡 S x Clsd J A = x S

Proof

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