Metamath Proof Explorer

Theorem cvmcov2

Description: The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-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 cvmcov2 
|- ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) -> E. x e. ~P U ( 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 simp1 
 |-  ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) -> F e. ( C CovMap J ) )
3 simp3 
 |-  ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) -> P e. U )
4 simp2 
 |-  ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) -> U e. J )
5 elunii 
 |-  ( ( P e. U /\ U e. J ) -> P e. U. J )
6 3 4 5 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) -> P e. U. J )
7 eqid 
 |-  U. J = U. J
8 1 7 cvmcov 
 |-  ( ( F e. ( C CovMap J ) /\ P e. U. J ) -> E. y e. J ( P e. y /\ ( S ` y ) =/= (/) ) )
9 2 6 8 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) -> E. y e. J ( P e. y /\ ( S ` y ) =/= (/) ) )
10 inss2 
 |-  ( y i^i U ) C_ U
11 vex 
 |-  y e. _V
12 11 inex1 
 |-  ( y i^i U ) e. _V
13 12 elpw 
 |-  ( ( y i^i U ) e. ~P U <-> ( y i^i U ) C_ U )
14 10 13 mpbir 
 |-  ( y i^i U ) e. ~P U
15 14 a1i 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> ( y i^i U ) e. ~P U )
16 simprrl 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> P e. y )
17 3 adantr 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> P e. U )
18 16 17 elind 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> P e. ( y i^i U ) )
19 simprrr 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> ( S ` y ) =/= (/) )
20 2 adantr 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> F e. ( C CovMap J ) )
21 cvmtop2 
 |-  ( F e. ( C CovMap J ) -> J e. Top )
22 20 21 syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> J e. Top )
23 simprl 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> y e. J )
24 4 adantr 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> U e. J )
25 inopn 
 |-  ( ( J e. Top /\ y e. J /\ U e. J ) -> ( y i^i U ) e. J )
26 22 23 24 25 syl3anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> ( y i^i U ) e. J )
27 inss1 
 |-  ( y i^i U ) C_ y
28 27 a1i 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> ( y i^i U ) C_ y )
29 1 cvmsss2 
 |-  ( ( F e. ( C CovMap J ) /\ ( y i^i U ) e. J /\ ( y i^i U ) C_ y ) -> ( ( S ` y ) =/= (/) -> ( S ` ( y i^i U ) ) =/= (/) ) )
30 20 26 28 29 syl3anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> ( ( S ` y ) =/= (/) -> ( S ` ( y i^i U ) ) =/= (/) ) )
31 19 30 mpd 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> ( S ` ( y i^i U ) ) =/= (/) )
32 eleq2 
 |-  ( x = ( y i^i U ) -> ( P e. x <-> P e. ( y i^i U ) ) )
33 fveq2 
 |-  ( x = ( y i^i U ) -> ( S ` x ) = ( S ` ( y i^i U ) ) )
34 33 neeq1d 
 |-  ( x = ( y i^i U ) -> ( ( S ` x ) =/= (/) <-> ( S ` ( y i^i U ) ) =/= (/) ) )
35 32 34 anbi12d 
 |-  ( x = ( y i^i U ) -> ( ( P e. x /\ ( S ` x ) =/= (/) ) <-> ( P e. ( y i^i U ) /\ ( S ` ( y i^i U ) ) =/= (/) ) ) )
36 35 rspcev 
 |-  ( ( ( y i^i U ) e. ~P U /\ ( P e. ( y i^i U ) /\ ( S ` ( y i^i U ) ) =/= (/) ) ) -> E. x e. ~P U ( P e. x /\ ( S ` x ) =/= (/) ) )
37 15 18 31 36 syl12anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) /\ ( y e. J /\ ( P e. y /\ ( S ` y ) =/= (/) ) ) ) -> E. x e. ~P U ( P e. x /\ ( S ` x ) =/= (/) ) )
38 9 37 rexlimddv 
 |-  ( ( F e. ( C CovMap J ) /\ U e. J /\ P e. U ) -> E. x e. ~P U ( P e. x /\ ( S ` x ) =/= (/) ) )