Metamath Proof Explorer

Theorem cvmscld

Description: The sets of an even covering are clopen in the subspace topology on T . (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypothesis cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion cvmscld ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) )

Proof

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 eqtrid ⊢ ( ( 𝐹 ∈ ( 𝐶 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 biimtrid ⊢ ( ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑥 ≠ 𝐴 → ( 𝐴 ∩ 𝑥 ) = ∅ ) )
42 41 impr ⊢ ( ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑥 ≠ 𝐴 ) ) → ( 𝐴 ∩ 𝑥 ) = ∅ )
43 36 42 sylan2b ⊢ ( ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) ∧ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ) → ( 𝐴 ∩ 𝑥 ) = ∅ )
44 43 iuneq2dv ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑥 ) = ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ∅ )
45 44 3adant1 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑥 ) = ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ∅ )
46 iun0 ⊢ ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ∅ = ∅
47 45 46 eqtrdi ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ∪ 𝑥 ∈ ( 𝑇 ∖ { 𝐴 } ) ( 𝐴 ∩ 𝑥 ) = ∅ )
48 35 47 eqtrid ⊢ ( ( 𝐹 ∈ ( 𝐶 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 dfss2 ⊢ ( 𝑥 ⊆ ( ◡ 𝐹 “ 𝑈 ) ↔ ( 𝑥 ∩ ( ◡ 𝐹 “ 𝑈 ) ) = 𝑥 )
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 ( ◡ 𝐹 “ 𝑈 ) ) ) )