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 bitrid ⊢ ( ( 𝐽 ∈ 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 ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )