Step |
Hyp |
Ref |
Expression |
1 |
|
cvmcov.1 |
⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) |
2 |
|
cvmtop1 |
⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top ) |
3 |
2
|
3ad2ant1 |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐶 ∈ Top ) |
4 |
1
|
cvmsuni |
⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ) |
5 |
4
|
3ad2ant2 |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ) |
6 |
1
|
cvmsss |
⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑇 ⊆ 𝐶 ) |
7 |
6
|
3ad2ant2 |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ⊆ 𝐶 ) |
8 |
7
|
unissd |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝑇 ⊆ ∪ 𝐶 ) |
9 |
5 8
|
eqsstrrd |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ◡ 𝐹 “ 𝑈 ) ⊆ ∪ 𝐶 ) |
10 |
|
eqid |
⊢ ∪ 𝐶 = ∪ 𝐶 |
11 |
10
|
restuni |
⊢ ( ( 𝐶 ∈ Top ∧ ( ◡ 𝐹 “ 𝑈 ) ⊆ ∪ 𝐶 ) → ( ◡ 𝐹 “ 𝑈 ) = ∪ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
12 |
3 9 11
|
syl2anc |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ◡ 𝐹 “ 𝑈 ) = ∪ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
13 |
12
|
difeq1d |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ( ◡ 𝐹 “ 𝑈 ) ∖ ∪ ( 𝑇 ∖ { 𝐴 } ) ) = ( ∪ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ∖ ∪ ( 𝑇 ∖ { 𝐴 } ) ) ) |
14 |
|
unisng |
⊢ ( 𝐴 ∈ 𝑇 → ∪ { 𝐴 } = 𝐴 ) |
15 |
14
|
3ad2ant3 |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ { 𝐴 } = 𝐴 ) |
16 |
15
|
uneq2d |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∪ ∪ { 𝐴 } ) = ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∪ 𝐴 ) ) |
17 |
|
uniun |
⊢ ∪ ( ( 𝑇 ∖ { 𝐴 } ) ∪ { 𝐴 } ) = ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∪ ∪ { 𝐴 } ) |
18 |
|
undif1 |
⊢ ( ( 𝑇 ∖ { 𝐴 } ) ∪ { 𝐴 } ) = ( 𝑇 ∪ { 𝐴 } ) |
19 |
|
simp3 |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ∈ 𝑇 ) |
20 |
19
|
snssd |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → { 𝐴 } ⊆ 𝑇 ) |
21 |
|
ssequn2 |
⊢ ( { 𝐴 } ⊆ 𝑇 ↔ ( 𝑇 ∪ { 𝐴 } ) = 𝑇 ) |
22 |
20 21
|
sylib |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝑇 ∪ { 𝐴 } ) = 𝑇 ) |
23 |
18 22
|
syl5eq |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ( 𝑇 ∖ { 𝐴 } ) ∪ { 𝐴 } ) = 𝑇 ) |
24 |
23
|
unieqd |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ ( ( 𝑇 ∖ { 𝐴 } ) ∪ { 𝐴 } ) = ∪ 𝑇 ) |
25 |
24 5
|
eqtrd |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ ( ( 𝑇 ∖ { 𝐴 } ) ∪ { 𝐴 } ) = ( ◡ 𝐹 “ 𝑈 ) ) |
26 |
17 25
|
eqtr3id |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∪ ∪ { 𝐴 } ) = ( ◡ 𝐹 “ 𝑈 ) ) |
27 |
16 26
|
eqtr3d |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∪ 𝐴 ) = ( ◡ 𝐹 “ 𝑈 ) ) |
28 |
|
difss |
⊢ ( 𝑇 ∖ { 𝐴 } ) ⊆ 𝑇 |
29 |
28
|
unissi |
⊢ ∪ ( 𝑇 ∖ { 𝐴 } ) ⊆ ∪ 𝑇 |
30 |
29 5
|
sseqtrid |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ ( 𝑇 ∖ { 𝐴 } ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) |
31 |
|
uniiun |
⊢ ∪ ( 𝑇 ∖ { 𝐴 } ) = ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) 𝑥 |
32 |
31
|
ineq2i |
⊢ ( 𝐴 ∩ ∪ ( 𝑇 ∖ { 𝐴 } ) ) = ( 𝐴 ∩ ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) 𝑥 ) |
33 |
|
incom |
⊢ ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∩ 𝐴 ) = ( 𝐴 ∩ ∪ ( 𝑇 ∖ { 𝐴 } ) ) |
34 |
|
iunin2 |
⊢ ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑥 ) = ( 𝐴 ∩ ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) 𝑥 ) |
35 |
32 33 34
|
3eqtr4i |
⊢ ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∩ 𝐴 ) = ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑥 ) |
36 |
|
eldifsn |
⊢ ( 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ↔ ( 𝑥 ∈ 𝑇 ∧ 𝑥 ≠ 𝐴 ) ) |
37 |
|
nesym |
⊢ ( 𝑥 ≠ 𝐴 ↔ ¬ 𝐴 = 𝑥 ) |
38 |
1
|
cvmsdisj |
⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐴 = 𝑥 ∨ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) |
39 |
38
|
3expa |
⊢ ( ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐴 = 𝑥 ∨ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) |
40 |
39
|
ord |
⊢ ( ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( ¬ 𝐴 = 𝑥 → ( 𝐴 ∩ 𝑥 ) = ∅ ) ) |
41 |
37 40
|
syl5bi |
⊢ ( ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑥 ≠ 𝐴 → ( 𝐴 ∩ 𝑥 ) = ∅ ) ) |
42 |
41
|
impr |
⊢ ( ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑥 ≠ 𝐴 ) ) → ( 𝐴 ∩ 𝑥 ) = ∅ ) |
43 |
36 42
|
sylan2b |
⊢ ( ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ) → ( 𝐴 ∩ 𝑥 ) = ∅ ) |
44 |
43
|
iuneq2dv |
⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑥 ) = ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ∅ ) |
45 |
44
|
3adant1 |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑥 ) = ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ∅ ) |
46 |
|
iun0 |
⊢ ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ∅ = ∅ |
47 |
45 46
|
eqtrdi |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑥 ) = ∅ ) |
48 |
35 47
|
syl5eq |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∩ 𝐴 ) = ∅ ) |
49 |
|
uneqdifeq |
⊢ ( ( ∪ ( 𝑇 ∖ { 𝐴 } ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ∧ ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∩ 𝐴 ) = ∅ ) → ( ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∪ 𝐴 ) = ( ◡ 𝐹 “ 𝑈 ) ↔ ( ( ◡ 𝐹 “ 𝑈 ) ∖ ∪ ( 𝑇 ∖ { 𝐴 } ) ) = 𝐴 ) ) |
50 |
30 48 49
|
syl2anc |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ( ∪ ( 𝑇 ∖ { 𝐴 } ) ∪ 𝐴 ) = ( ◡ 𝐹 “ 𝑈 ) ↔ ( ( ◡ 𝐹 “ 𝑈 ) ∖ ∪ ( 𝑇 ∖ { 𝐴 } ) ) = 𝐴 ) ) |
51 |
27 50
|
mpbid |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ( ◡ 𝐹 “ 𝑈 ) ∖ ∪ ( 𝑇 ∖ { 𝐴 } ) ) = 𝐴 ) |
52 |
13 51
|
eqtr3d |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ∪ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ∖ ∪ ( 𝑇 ∖ { 𝐴 } ) ) = 𝐴 ) |
53 |
|
uniexg |
⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ∪ 𝑇 ∈ V ) |
54 |
53
|
3ad2ant2 |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝑇 ∈ V ) |
55 |
5 54
|
eqeltrrd |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ◡ 𝐹 “ 𝑈 ) ∈ V ) |
56 |
|
resttop |
⊢ ( ( 𝐶 ∈ Top ∧ ( ◡ 𝐹 “ 𝑈 ) ∈ V ) → ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ∈ Top ) |
57 |
3 55 56
|
syl2anc |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ∈ Top ) |
58 |
|
elssuni |
⊢ ( 𝑥 ∈ 𝑇 → 𝑥 ⊆ ∪ 𝑇 ) |
59 |
58
|
adantl |
⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ⊆ ∪ 𝑇 ) |
60 |
5
|
adantr |
⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ) |
61 |
59 60
|
sseqtrd |
⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ⊆ ( ◡ 𝐹 “ 𝑈 ) ) |
62 |
|
df-ss |
⊢ ( 𝑥 ⊆ ( ◡ 𝐹 “ 𝑈 ) ↔ ( 𝑥 ∩ ( ◡ 𝐹 “ 𝑈 ) ) = 𝑥 ) |
63 |
61 62
|
sylib |
⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑥 ∩ ( ◡ 𝐹 “ 𝑈 ) ) = 𝑥 ) |
64 |
3
|
adantr |
⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → 𝐶 ∈ Top ) |
65 |
55
|
adantr |
⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( ◡ 𝐹 “ 𝑈 ) ∈ V ) |
66 |
7
|
sselda |
⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ 𝐶 ) |
67 |
|
elrestr |
⊢ ( ( 𝐶 ∈ Top ∧ ( ◡ 𝐹 “ 𝑈 ) ∈ V ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∩ ( ◡ 𝐹 “ 𝑈 ) ) ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
68 |
64 65 66 67
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑥 ∩ ( ◡ 𝐹 “ 𝑈 ) ) ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
69 |
63 68
|
eqeltrrd |
⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
70 |
69
|
ex |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
71 |
70
|
ssrdv |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ⊆ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
72 |
71
|
ssdifssd |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝑇 ∖ { 𝐴 } ) ⊆ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
73 |
|
uniopn |
⊢ ( ( ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ∈ Top ∧ ( 𝑇 ∖ { 𝐴 } ) ⊆ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) → ∪ ( 𝑇 ∖ { 𝐴 } ) ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
74 |
57 72 73
|
syl2anc |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ ( 𝑇 ∖ { 𝐴 } ) ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
75 |
|
eqid |
⊢ ∪ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) = ∪ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) |
76 |
75
|
opncld |
⊢ ( ( ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ∈ Top ∧ ∪ ( 𝑇 ∖ { 𝐴 } ) ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) → ( ∪ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ∖ ∪ ( 𝑇 ∖ { 𝐴 } ) ) ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
77 |
57 74 76
|
syl2anc |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( ∪ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ∖ ∪ ( 𝑇 ∖ { 𝐴 } ) ) ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
78 |
52 77
|
eqeltrrd |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) |