Metamath Proof Explorer

Theorem iscvm

Description: The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Hypotheses iscvm.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 ) ) ) ) } )
iscvm.2 
|- X = U. J
Assertion 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 ) =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 iscvm.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 iscvm.2 
 |-  X = U. J
3 anass 
 |-  ( ( ( ( C e. Top /\ J e. Top ) /\ F e. ( C Cn J ) ) /\ A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) ) <-> ( ( 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 df-3an 
 |-  ( ( C e. Top /\ J e. Top /\ F e. ( C Cn J ) ) <-> ( ( C e. Top /\ J e. Top ) /\ F e. ( C Cn J ) ) )
5 4 anbi1i 
 |-  ( ( ( C e. Top /\ J e. Top /\ F e. ( C Cn J ) ) /\ A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) ) <-> ( ( ( C e. Top /\ J e. Top ) /\ F e. ( C Cn J ) ) /\ A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) ) )
6 df-cvm 
 |-  CovMap = ( c e. Top , j e. Top |-> { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. 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 ) ) ) ) ) } )
7 6 elmpocl 
 |-  ( F e. ( C CovMap J ) -> ( C e. Top /\ J e. Top ) )
8 oveq12 
 |-  ( ( c = C /\ j = J ) -> ( c Cn j ) = ( C Cn J ) )
9 simpr 
 |-  ( ( c = C /\ j = J ) -> j = J )
10 9 unieqd 
 |-  ( ( c = C /\ j = J ) -> U. j = U. J )
11 10 2 eqtr4di 
 |-  ( ( c = C /\ j = J ) -> U. j = X )
12 simpl 
 |-  ( ( c = C /\ j = J ) -> c = C )
13 12 pweqd 
 |-  ( ( c = C /\ j = J ) -> ~P c = ~P C )
14 13 difeq1d 
 |-  ( ( c = C /\ j = J ) -> ( ~P c \ { (/) } ) = ( ~P C \ { (/) } ) )
15 oveq1 
 |-  ( c = C -> ( c |`t u ) = ( C |`t u ) )
16 oveq1 
 |-  ( j = J -> ( j |`t k ) = ( J |`t k ) )
17 15 16 oveqan12d 
 |-  ( ( c = C /\ j = J ) -> ( ( c |`t u ) Homeo ( j |`t k ) ) = ( ( C |`t u ) Homeo ( J |`t k ) ) )
18 17 eleq2d 
 |-  ( ( c = C /\ j = J ) -> ( ( f |` u ) e. ( ( c |`t u ) Homeo ( j |`t k ) ) <-> ( f |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) )
19 18 anbi2d 
 |-  ( ( c = C /\ j = J ) -> ( ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c |`t u ) Homeo ( j |`t k ) ) ) <-> ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) )
20 19 ralbidv 
 |-  ( ( c = C /\ j = J ) -> ( A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( c |`t u ) Homeo ( j |`t k ) ) ) <-> A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) )
21 20 anbi2d 
 |-  ( ( c = C /\ j = J ) -> ( ( 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 ) ) ) ) <-> ( 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 ) ) ) ) ) )
22 14 21 rexeqbidv 
 |-  ( ( c = C /\ j = J ) -> ( E. 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 ) ) ) ) <-> E. 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 ) ) ) ) ) )
23 22 anbi2d 
 |-  ( ( c = C /\ j = J ) -> ( ( x e. k /\ E. 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 ) ) ) ) ) <-> ( x e. k /\ E. 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 ) ) ) ) ) ) )
24 9 23 rexeqbidv 
 |-  ( ( c = C /\ j = J ) -> ( E. k e. j ( x e. k /\ E. 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 ) ) ) ) ) <-> E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) ) )
25 11 24 raleqbidv 
 |-  ( ( c = C /\ j = J ) -> ( A. x e. U. j E. k e. j ( x e. k /\ E. 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 ) ) ) ) ) <-> A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) ) )
26 8 25 rabeqbidv 
 |-  ( ( c = C /\ j = J ) -> { f e. ( c Cn j ) | A. x e. U. j E. k e. j ( x e. k /\ E. 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 ) ) ) ) ) } = { f e. ( C Cn J ) | A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) } )
27 ovex 
 |-  ( C Cn J ) e. _V
28 27 rabex 
 |-  { f e. ( C Cn J ) | A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) } e. _V
29 26 6 28 ovmpoa 
 |-  ( ( C e. Top /\ J e. Top ) -> ( C CovMap J ) = { f e. ( C Cn J ) | A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) } )
30 29 eleq2d 
 |-  ( ( C e. Top /\ J e. Top ) -> ( F e. ( C CovMap J ) <-> F e. { f e. ( C Cn J ) | A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) } ) )
31 id 
 |-  ( k e. J -> k e. J )
32 pwexg 
 |-  ( C e. Top -> ~P C e. _V )
33 32 adantr 
 |-  ( ( C e. Top /\ J e. Top ) -> ~P C e. _V )
34 difexg 
 |-  ( ~P C e. _V -> ( ~P C \ { (/) } ) e. _V )
35 rabexg 
 |-  ( ( ~P C \ { (/) } ) e. _V -> { 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 ) ) ) ) } e. _V )
36 33 34 35 3syl 
 |-  ( ( C e. Top /\ J e. Top ) -> { 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 ) ) ) ) } e. _V )
37 1 fvmpt2 
 |-  ( ( 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 ) ) ) ) } e. _V ) -> ( S ` k ) = { 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 ) ) ) ) } )
38 31 36 37 syl2anr 
 |-  ( ( ( C e. Top /\ J e. Top ) /\ k e. J ) -> ( S ` k ) = { 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 ) ) ) ) } )
39 38 neeq1d 
 |-  ( ( ( C e. Top /\ J e. Top ) /\ k e. J ) -> ( ( S ` k ) =/= (/) <-> { 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 ) ) ) ) } =/= (/) ) )
40 rabn0 
 |-  ( { 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 ) ) ) ) } =/= (/) <-> E. 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 ) ) ) ) )
41 39 40 bitrdi 
 |-  ( ( ( C e. Top /\ J e. Top ) /\ k e. J ) -> ( ( S ` k ) =/= (/) <-> E. 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 ) ) ) ) ) )
42 41 anbi2d 
 |-  ( ( ( C e. Top /\ J e. Top ) /\ k e. J ) -> ( ( x e. k /\ ( S ` k ) =/= (/) ) <-> ( x e. k /\ E. 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 ) ) ) ) ) ) )
43 42 rexbidva 
 |-  ( ( C e. Top /\ J e. Top ) -> ( E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) <-> E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) ) )
44 43 ralbidv 
 |-  ( ( C e. Top /\ J e. Top ) -> ( A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) <-> A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) ) )
45 44 anbi2d 
 |-  ( ( C e. Top /\ J e. Top ) -> ( ( F e. ( C Cn J ) /\ A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) ) <-> ( F e. ( C Cn J ) /\ A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) ) ) )
46 cnveq 
 |-  ( f = F -> `' f = `' F )
47 46 imaeq1d 
 |-  ( f = F -> ( `' f " k ) = ( `' F " k ) )
48 47 eqeq2d 
 |-  ( f = F -> ( U. s = ( `' f " k ) <-> U. s = ( `' F " k ) ) )
49 reseq1 
 |-  ( f = F -> ( f |` u ) = ( F |` u ) )
50 49 eleq1d 
 |-  ( f = F -> ( ( f |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) <-> ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) )
51 50 anbi2d 
 |-  ( f = F -> ( ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) <-> ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) )
52 51 ralbidv 
 |-  ( f = F -> ( A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( f |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) <-> A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) )
53 48 52 anbi12d 
 |-  ( f = F -> ( ( 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 ) ) ) ) <-> ( 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 ) ) ) ) ) )
54 53 rexbidv 
 |-  ( f = F -> ( E. 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 ) ) ) ) <-> E. 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 ) ) ) ) ) )
55 54 anbi2d 
 |-  ( f = F -> ( ( x e. k /\ E. 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 ) ) ) ) ) <-> ( x e. k /\ E. 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 ) ) ) ) ) ) )
56 55 rexbidv 
 |-  ( f = F -> ( E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) <-> E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) ) )
57 56 ralbidv 
 |-  ( f = F -> ( A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) <-> A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) ) )
58 57 elrab 
 |-  ( F e. { f e. ( C Cn J ) | A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) } <-> ( F e. ( C Cn J ) /\ A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) ) )
59 45 58 bitr4di 
 |-  ( ( C e. Top /\ J e. Top ) -> ( ( F e. ( C Cn J ) /\ A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) ) <-> F e. { f e. ( C Cn J ) | A. x e. X E. k e. J ( x e. k /\ E. 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 ) ) ) ) ) } ) )
60 30 59 bitr4d 
 |-  ( ( C e. Top /\ J e. Top ) -> ( F e. ( C CovMap J ) <-> ( F e. ( C Cn J ) /\ A. x e. X E. k e. J ( x e. k /\ ( S ` k ) =/= (/) ) ) ) )
61 7 60 biadanii 
 |-  ( 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 ) =/= (/) ) ) ) )
62 3 5 61 3bitr4ri 
 |-  ( 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 ) =/= (/) ) ) )