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 ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ) |