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 syl5eq
 |-  ( ( 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 syl5bi
 |-  ( ( ( 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 syl5eq
 |-  ( ( 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 df-ss
 |-  ( 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 ) ) ) )