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