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 𝑋 = 𝐽
restcls.2 𝐾 = ( 𝐽t 𝑌 )
Assertion restcls ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 restcls.1 𝑋 = 𝐽
2 restcls.2 𝐾 = ( 𝐽t 𝑌 )
3 simp1 ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → 𝐽 ∈ Top )
4 sstr ( ( 𝑆𝑌𝑌𝑋 ) → 𝑆𝑋 )
5 4 ancoms ( ( 𝑌𝑋𝑆𝑌 ) → 𝑆𝑋 )
6 5 3adant1 ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → 𝑆𝑋 )
7 1 clscld ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
8 3 6 7 syl2anc ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
9 eqid ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 )
10 ineq1 ( 𝑥 = ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ( 𝑥𝑌 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )
11 10 rspceeqv ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) = ( 𝑥𝑌 ) )
12 8 9 11 sylancl ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) = ( 𝑥𝑌 ) )
13 2 fveq2i ( Clsd ‘ 𝐾 ) = ( Clsd ‘ ( 𝐽t 𝑌 ) )
14 13 eleq2i ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ∈ ( Clsd ‘ 𝐾 ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ∈ ( Clsd ‘ ( 𝐽t 𝑌 ) ) )
15 1 restcld ( ( 𝐽 ∈ Top ∧ 𝑌𝑋 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ∈ ( Clsd ‘ ( 𝐽t 𝑌 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) = ( 𝑥𝑌 ) ) )
16 15 3adant3 ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ∈ ( Clsd ‘ ( 𝐽t 𝑌 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) = ( 𝑥𝑌 ) ) )
17 14 16 syl5bb ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ∈ ( Clsd ‘ 𝐾 ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) = ( 𝑥𝑌 ) ) )
18 12 17 mpbird ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ∈ ( Clsd ‘ 𝐾 ) )
19 1 sscls ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
20 3 6 19 syl2anc ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
21 simp3 ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → 𝑆𝑌 )
22 20 21 ssind ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → 𝑆 ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )
23 eqid 𝐾 = 𝐾
24 23 clsss2 ( ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ∈ ( Clsd ‘ 𝐾 ) ∧ 𝑆 ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )
25 18 22 24 syl2anc ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )
26 2 fveq2i ( cls ‘ 𝐾 ) = ( cls ‘ ( 𝐽t 𝑌 ) )
27 26 fveq1i ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( ( cls ‘ ( 𝐽t 𝑌 ) ) ‘ 𝑆 )
28 id ( 𝑌𝑋𝑌𝑋 )
29 1 topopn ( 𝐽 ∈ Top → 𝑋𝐽 )
30 ssexg ( ( 𝑌𝑋𝑋𝐽 ) → 𝑌 ∈ V )
31 28 29 30 syl2anr ( ( 𝐽 ∈ Top ∧ 𝑌𝑋 ) → 𝑌 ∈ V )
32 resttop ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ V ) → ( 𝐽t 𝑌 ) ∈ Top )
33 31 32 syldan ( ( 𝐽 ∈ Top ∧ 𝑌𝑋 ) → ( 𝐽t 𝑌 ) ∈ Top )
34 33 3adant3 ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( 𝐽t 𝑌 ) ∈ Top )
35 1 restuni ( ( 𝐽 ∈ Top ∧ 𝑌𝑋 ) → 𝑌 = ( 𝐽t 𝑌 ) )
36 35 3adant3 ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → 𝑌 = ( 𝐽t 𝑌 ) )
37 21 36 sseqtrd ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → 𝑆 ( 𝐽t 𝑌 ) )
38 eqid ( 𝐽t 𝑌 ) = ( 𝐽t 𝑌 )
39 38 clscld ( ( ( 𝐽t 𝑌 ) ∈ Top ∧ 𝑆 ( 𝐽t 𝑌 ) ) → ( ( cls ‘ ( 𝐽t 𝑌 ) ) ‘ 𝑆 ) ∈ ( Clsd ‘ ( 𝐽t 𝑌 ) ) )
40 34 37 39 syl2anc ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( cls ‘ ( 𝐽t 𝑌 ) ) ‘ 𝑆 ) ∈ ( Clsd ‘ ( 𝐽t 𝑌 ) ) )
41 27 40 eqeltrid ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Clsd ‘ ( 𝐽t 𝑌 ) ) )
42 1 restcld ( ( 𝐽 ∈ Top ∧ 𝑌𝑋 ) → ( ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Clsd ‘ ( 𝐽t 𝑌 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) ) )
43 42 3adant3 ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Clsd ‘ ( 𝐽t 𝑌 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) ) )
44 41 43 mpbid ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) )
45 2 33 eqeltrid ( ( 𝐽 ∈ Top ∧ 𝑌𝑋 ) → 𝐾 ∈ Top )
46 45 3adant3 ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → 𝐾 ∈ Top )
47 2 unieqi 𝐾 = ( 𝐽t 𝑌 )
48 47 eqcomi ( 𝐽t 𝑌 ) = 𝐾
49 48 sscls ( ( 𝐾 ∈ Top ∧ 𝑆 ( 𝐽t 𝑌 ) ) → 𝑆 ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) )
50 46 37 49 syl2anc ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → 𝑆 ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) )
51 50 adantr ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) ) ) → 𝑆 ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) )
52 inss1 ( 𝑥𝑌 ) ⊆ 𝑥
53 sseq1 ( ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) → ( ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ⊆ 𝑥 ↔ ( 𝑥𝑌 ) ⊆ 𝑥 ) )
54 52 53 mpbiri ( ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ⊆ 𝑥 )
55 54 ad2antll ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) ) ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ⊆ 𝑥 )
56 51 55 sstrd ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) ) ) → 𝑆𝑥 )
57 1 clsss2 ( ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆𝑥 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑥 )
58 57 adantl ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑥 )
59 58 ssrind ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆𝑥 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ⊆ ( 𝑥𝑌 ) )
60 sseq2 ( ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ⊆ ( 𝑥𝑌 ) ) )
61 59 60 syl5ibrcom ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆𝑥 ) ) → ( ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) )
62 61 expr ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑆𝑥 → ( ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ) )
63 62 com23 ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) → ( 𝑆𝑥 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ) )
64 63 impr ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) ) ) → ( 𝑆𝑥 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) )
65 56 64 mpd ( ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑥𝑌 ) ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) )
66 44 65 rexlimddv ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) )
67 25 66 eqssd ( ( 𝐽 ∈ Top ∧ 𝑌𝑋𝑆𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )