Metamath Proof Explorer

Theorem cvmcov

Description: Property of a covering map. In order to make the covering property more manageable, we define here the set S ( k ) of all even coverings of an open set k in the range. Then the covering property states that every point has a neighborhood which has an even covering. (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Hypotheses 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 ) ) ) ) } )
cvmcov.2 
|- X = U. J
Assertion cvmcov 
|- ( ( F e. ( C CovMap J ) /\ P e. X ) -> E. x e. J ( P e. x /\ ( S ` x ) =/= (/) ) )

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 cvmcov.2 
 |-  X = U. J
3 1 2 iscvm 
 |-  ( F e. ( C CovMap J ) <-> ( ( C e. Top /\ J e. Top /\ F e. ( C Cn J ) ) /\ A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) ) )
4 3 simprbi 
 |-  ( F e. ( C CovMap J ) -> A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) )
5 eleq1 
 |-  ( x = P -> ( x e. k <-> P e. k ) )
6 5 anbi1d 
 |-  ( x = P -> ( ( x e. k /\ ( S ` k ) =/= (/) ) <-> ( P e. k /\ ( S ` k ) =/= (/) ) ) )
7 6 rexbidv 
 |-  ( x = P -> ( E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) <-> E. k e. J ( P e. k /\ ( S ` k ) =/= (/) ) ) )
8 7 rspcv 
 |-  ( P e. X -> ( A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) -> E. k e. J ( P e. k /\ ( S ` k ) =/= (/) ) ) )
9 4 8 mpan9 
 |-  ( ( F e. ( C CovMap J ) /\ P e. X ) -> E. k e. J ( P e. k /\ ( S ` k ) =/= (/) ) )
10 nfv 
 |-  F/ k P e. x
11 nfmpt1 
 |-  F/_ k ( 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 ) ) ) ) } )
12 1 11 nfcxfr 
 |-  F/_ k S
13 nfcv 
 |-  F/_ k x
14 12 13 nffv 
 |-  F/_ k ( S ` x )
15 nfcv 
 |-  F/_ k (/)
16 14 15 nfne 
 |-  F/ k ( S ` x ) =/= (/)
17 10 16 nfan 
 |-  F/ k ( P e. x /\ ( S ` x ) =/= (/) )
18 nfv 
 |-  F/ x ( P e. k /\ ( S ` k ) =/= (/) )
19 eleq2w 
 |-  ( x = k -> ( P e. x <-> P e. k ) )
20 fveq2 
 |-  ( x = k -> ( S ` x ) = ( S ` k ) )
21 20 neeq1d 
 |-  ( x = k -> ( ( S ` x ) =/= (/) <-> ( S ` k ) =/= (/) ) )
22 19 21 anbi12d 
 |-  ( x = k -> ( ( P e. x /\ ( S ` x ) =/= (/) ) <-> ( P e. k /\ ( S ` k ) =/= (/) ) ) )
23 17 18 22 cbvrexw 
 |-  ( E. x e. J ( P e. x /\ ( S ` x ) =/= (/) ) <-> E. k e. J ( P e. k /\ ( S ` k ) =/= (/) ) )
24 9 23 sylibr 
 |-  ( ( F e. ( C CovMap J ) /\ P e. X ) -> E. x e. J ( P e. x /\ ( S ` x ) =/= (/) ) )