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 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 ( 𝐹𝑈 ) ) ) )