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 
|- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
Assertion cvmscld 
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> A e. ( Clsd ` ( C |`t ( `' F " U ) ) ) )

Proof

Step Hyp Ref Expression
1 cvmcov.1 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
3 2 3ad2ant1 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> C e. Top )
4 1 cvmsuni 
 |-  ( T e. ( S ` U ) -> U. T = ( `' F " U ) )
5 4 3ad2ant2 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. T = ( `' F " U ) )
6 1 cvmsss 
 |-  ( T e. ( S ` U ) -> T C_ C )
7 6 3ad2ant2 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> T C_ C )
8 7 unissd 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. T C_ U. C )
9 5 8 eqsstrrd 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( `' F " U ) C_ U. C )
10 eqid 
 |-  U. C = U. C
11 10 restuni 
 |-  ( ( C e. Top /\ ( `' F " U ) C_ U. C ) -> ( `' F " U ) = U. ( C |`t ( `' F " U ) ) )
12 3 9 11 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( `' F " U ) = U. ( C |`t ( `' F " U ) ) )
13 12 difeq1d 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( ( `' F " U ) \ U. ( T \ { A } ) ) = ( U. ( C |`t ( `' F " U ) ) \ U. ( T \ { A } ) ) )
14 unisng 
 |-  ( A e. T -> U. { A } = A )
15 14 3ad2ant3 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. { A } = A )
16 15 uneq2d 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( T \ { A } ) u. U. { A } ) = ( U. ( T \ { A } ) u. A ) )
17 uniun 
 |-  U. ( ( T \ { A } ) u. { A } ) = ( U. ( T \ { A } ) u. U. { A } )
18 undif1 
 |-  ( ( T \ { A } ) u. { A } ) = ( T u. { A } )
19 simp3 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> A e. T )
20 19 snssd 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> { A } C_ T )
21 ssequn2 
 |-  ( { A } C_ T <-> ( T u. { A } ) = T )
22 20 21 sylib 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( T u. { A } ) = T )
23 18 22 eqtrid 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( ( T \ { A } ) u. { A } ) = T )
24 23 unieqd 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. ( ( T \ { A } ) u. { A } ) = U. T )
25 24 5 eqtrd 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. ( ( T \ { A } ) u. { A } ) = ( `' F " U ) )
26 17 25 eqtr3id 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( T \ { A } ) u. U. { A } ) = ( `' F " U ) )
27 16 26 eqtr3d 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( T \ { A } ) u. A ) = ( `' F " U ) )
28 difss 
 |-  ( T \ { A } ) C_ T
29 28 unissi 
 |-  U. ( T \ { A } ) C_ U. T
30 29 5 sseqtrid 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. ( T \ { A } ) C_ ( `' F " U ) )
31 uniiun 
 |-  U. ( T \ { A } ) = U_ x e. ( T \ { A } ) x
32 31 ineq2i 
 |-  ( A i^i U. ( T \ { A } ) ) = ( A i^i U_ x e. ( T \ { A } ) x )
33 incom 
 |-  ( U. ( T \ { A } ) i^i A ) = ( A i^i U. ( T \ { A } ) )
34 iunin2 
 |-  U_ x e. ( T \ { A } ) ( A i^i x ) = ( A i^i U_ x e. ( T \ { A } ) x )
35 32 33 34 3eqtr4i 
 |-  ( U. ( T \ { A } ) i^i A ) = U_ x e. ( T \ { A } ) ( A i^i x )
36 eldifsn 
 |-  ( x e. ( T \ { A } ) <-> ( x e. T /\ x =/= A ) )
37 nesym 
 |-  ( x =/= A <-> -. A = x )
38 1 cvmsdisj 
 |-  ( ( T e. ( S ` U ) /\ A e. T /\ x e. T ) -> ( A = x \/ ( A i^i x ) = (/) ) )
39 38 3expa 
 |-  ( ( ( T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( A = x \/ ( A i^i x ) = (/) ) )
40 39 ord 
 |-  ( ( ( T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( -. A = x -> ( A i^i x ) = (/) ) )
41 37 40 biimtrid 
 |-  ( ( ( T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( x =/= A -> ( A i^i x ) = (/) ) )
42 41 impr 
 |-  ( ( ( T e. ( S ` U ) /\ A e. T ) /\ ( x e. T /\ x =/= A ) ) -> ( A i^i x ) = (/) )
43 36 42 sylan2b 
 |-  ( ( ( T e. ( S ` U ) /\ A e. T ) /\ x e. ( T \ { A } ) ) -> ( A i^i x ) = (/) )
44 43 iuneq2dv 
 |-  ( ( T e. ( S ` U ) /\ A e. T ) -> U_ x e. ( T \ { A } ) ( A i^i x ) = U_ x e. ( T \ { A } ) (/) )
45 44 3adant1 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U_ x e. ( T \ { A } ) ( A i^i x ) = U_ x e. ( T \ { A } ) (/) )
46 iun0 
 |-  U_ x e. ( T \ { A } ) (/) = (/)
47 45 46 eqtrdi 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U_ x e. ( T \ { A } ) ( A i^i x ) = (/) )
48 35 47 eqtrid 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( T \ { A } ) i^i A ) = (/) )
49 uneqdifeq 
 |-  ( ( U. ( T \ { A } ) C_ ( `' F " U ) /\ ( U. ( T \ { A } ) i^i A ) = (/) ) -> ( ( U. ( T \ { A } ) u. A ) = ( `' F " U ) <-> ( ( `' F " U ) \ U. ( T \ { A } ) ) = A ) )
50 30 48 49 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( ( U. ( T \ { A } ) u. A ) = ( `' F " U ) <-> ( ( `' F " U ) \ U. ( T \ { A } ) ) = A ) )
51 27 50 mpbid 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( ( `' F " U ) \ U. ( T \ { A } ) ) = A )
52 13 51 eqtr3d 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( C |`t ( `' F " U ) ) \ U. ( T \ { A } ) ) = A )
53 uniexg 
 |-  ( T e. ( S ` U ) -> U. T e. _V )
54 53 3ad2ant2 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. T e. _V )
55 5 54 eqeltrrd 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( `' F " U ) e. _V )
56 resttop 
 |-  ( ( C e. Top /\ ( `' F " U ) e. _V ) -> ( C |`t ( `' F " U ) ) e. Top )
57 3 55 56 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( C |`t ( `' F " U ) ) e. Top )
58 elssuni 
 |-  ( x e. T -> x C_ U. T )
59 58 adantl 
 |-  ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> x C_ U. T )
60 5 adantr 
 |-  ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> U. T = ( `' F " U ) )
61 59 60 sseqtrd 
 |-  ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> x C_ ( `' F " U ) )
62 dfss2 
 |-  ( x C_ ( `' F " U ) <-> ( x i^i ( `' F " U ) ) = x )
63 61 62 sylib 
 |-  ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( x i^i ( `' F " U ) ) = x )
64 3 adantr 
 |-  ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> C e. Top )
65 55 adantr 
 |-  ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( `' F " U ) e. _V )
66 7 sselda 
 |-  ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> x e. C )
67 elrestr 
 |-  ( ( C e. Top /\ ( `' F " U ) e. _V /\ x e. C ) -> ( x i^i ( `' F " U ) ) e. ( C |`t ( `' F " U ) ) )
68 64 65 66 67 syl3anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( x i^i ( `' F " U ) ) e. ( C |`t ( `' F " U ) ) )
69 63 68 eqeltrrd 
 |-  ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> x e. ( C |`t ( `' F " U ) ) )
70 69 ex 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( x e. T -> x e. ( C |`t ( `' F " U ) ) ) )
71 70 ssrdv 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> T C_ ( C |`t ( `' F " U ) ) )
72 71 ssdifssd 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( T \ { A } ) C_ ( C |`t ( `' F " U ) ) )
73 uniopn 
 |-  ( ( ( C |`t ( `' F " U ) ) e. Top /\ ( T \ { A } ) C_ ( C |`t ( `' F " U ) ) ) -> U. ( T \ { A } ) e. ( C |`t ( `' F " U ) ) )
74 57 72 73 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. ( T \ { A } ) e. ( C |`t ( `' F " U ) ) )
75 eqid 
 |-  U. ( C |`t ( `' F " U ) ) = U. ( C |`t ( `' F " U ) )
76 75 opncld 
 |-  ( ( ( C |`t ( `' F " U ) ) e. Top /\ U. ( T \ { A } ) e. ( C |`t ( `' F " U ) ) ) -> ( U. ( C |`t ( `' F " U ) ) \ U. ( T \ { A } ) ) e. ( Clsd ` ( C |`t ( `' F " U ) ) ) )
77 57 74 76 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( C |`t ( `' F " U ) ) \ U. ( T \ { A } ) ) e. ( Clsd ` ( C |`t ( `' F " U ) ) ) )
78 52 77 eqeltrrd 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> A e. ( Clsd ` ( C |`t ( `' F " U ) ) ) )