Metamath Proof Explorer

Theorem cvmlift3

Description: A general version of cvmlift . If K is simply connected and weakly locally path-connected, then there is a unique lift of functions on K which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015)

Ref Expression
Hypotheses cvmlift3.b 
|- B = U. C
cvmlift3.y 
|- Y = U. K
cvmlift3.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmlift3.k 
|- ( ph -> K e. SConn )
cvmlift3.l 
|- ( ph -> K e. N-Locally PConn )
cvmlift3.o 
|- ( ph -> O e. Y )
cvmlift3.g 
|- ( ph -> G e. ( K Cn J ) )
cvmlift3.p 
|- ( ph -> P e. B )
cvmlift3.e 
|- ( ph -> ( F ` P ) = ( G ` O ) )
Assertion cvmlift3 
|- ( ph -> E! f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) )

Proof

Step Hyp Ref Expression
1 cvmlift3.b 
 |-  B = U. C
2 cvmlift3.y 
 |-  Y = U. K
3 cvmlift3.f 
 |-  ( ph -> F e. ( C CovMap J ) )
4 cvmlift3.k 
 |-  ( ph -> K e. SConn )
5 cvmlift3.l 
 |-  ( ph -> K e. N-Locally PConn )
6 cvmlift3.o 
 |-  ( ph -> O e. Y )
7 cvmlift3.g 
 |-  ( ph -> G e. ( K Cn J ) )
8 cvmlift3.p 
 |-  ( ph -> P e. B )
9 cvmlift3.e 
 |-  ( ph -> ( F ` P ) = ( G ` O ) )
10 eqeq2 
 |-  ( b = z -> ( ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = b <-> ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = z ) )
11 10 3anbi3d 
 |-  ( b = z -> ( ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = b ) <-> ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = z ) ) )
12 11 rexbidv 
 |-  ( b = z -> ( E. c e. ( II Cn K ) ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = b ) <-> E. c e. ( II Cn K ) ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = z ) ) )
13 12 cbvriotavw 
 |-  ( iota_ b e. B E. c e. ( II Cn K ) ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = b ) ) = ( iota_ z e. B E. c e. ( II Cn K ) ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = z ) )
14 fveq1 
 |-  ( c = f -> ( c ` 0 ) = ( f ` 0 ) )
15 14 eqeq1d 
 |-  ( c = f -> ( ( c ` 0 ) = O <-> ( f ` 0 ) = O ) )
16 fveq1 
 |-  ( c = f -> ( c ` 1 ) = ( f ` 1 ) )
17 16 eqeq1d 
 |-  ( c = f -> ( ( c ` 1 ) = a <-> ( f ` 1 ) = a ) )
18 coeq2 
 |-  ( d = g -> ( F o. d ) = ( F o. g ) )
19 18 eqeq1d 
 |-  ( d = g -> ( ( F o. d ) = ( G o. c ) <-> ( F o. g ) = ( G o. c ) ) )
20 fveq1 
 |-  ( d = g -> ( d ` 0 ) = ( g ` 0 ) )
21 20 eqeq1d 
 |-  ( d = g -> ( ( d ` 0 ) = P <-> ( g ` 0 ) = P ) )
22 19 21 anbi12d 
 |-  ( d = g -> ( ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) <-> ( ( F o. g ) = ( G o. c ) /\ ( g ` 0 ) = P ) ) )
23 22 cbvriotavw 
 |-  ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. c ) /\ ( g ` 0 ) = P ) )
24 coeq2 
 |-  ( c = f -> ( G o. c ) = ( G o. f ) )
25 24 eqeq2d 
 |-  ( c = f -> ( ( F o. g ) = ( G o. c ) <-> ( F o. g ) = ( G o. f ) ) )
26 25 anbi1d 
 |-  ( c = f -> ( ( ( F o. g ) = ( G o. c ) /\ ( g ` 0 ) = P ) <-> ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) )
27 26 riotabidv 
 |-  ( c = f -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. c ) /\ ( g ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) )
28 23 27 eqtrid 
 |-  ( c = f -> ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) )
29 28 fveq1d 
 |-  ( c = f -> ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) )
30 29 eqeq1d 
 |-  ( c = f -> ( ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = z <-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) )
31 15 17 30 3anbi123d 
 |-  ( c = f -> ( ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = z ) <-> ( ( f ` 0 ) = O /\ ( f ` 1 ) = a /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
32 31 cbvrexvw 
 |-  ( E. c e. ( II Cn K ) ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = z ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = a /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) )
33 eqeq2 
 |-  ( a = x -> ( ( f ` 1 ) = a <-> ( f ` 1 ) = x ) )
34 33 3anbi2d 
 |-  ( a = x -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = a /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
35 34 rexbidv 
 |-  ( a = x -> ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = a /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
36 32 35 syl5bb 
 |-  ( a = x -> ( E. c e. ( II Cn K ) ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = z ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
37 36 riotabidv 
 |-  ( a = x -> ( iota_ z e. B E. c e. ( II Cn K ) ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = z ) ) = ( iota_ z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
38 13 37 eqtrid 
 |-  ( a = x -> ( iota_ b e. B E. c e. ( II Cn K ) ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = b ) ) = ( iota_ z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
39 38 cbvmptv 
 |-  ( a e. Y |-> ( iota_ b e. B E. c e. ( II Cn K ) ( ( c ` 0 ) = O /\ ( c ` 1 ) = a /\ ( ( iota_ d e. ( II Cn C ) ( ( F o. d ) = ( G o. c ) /\ ( d ` 0 ) = P ) ) ` 1 ) = b ) ) ) = ( x e. Y |-> ( iota_ z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
40 eqid 
 |-  ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. c e. s ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) } ) = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. c e. s ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) } )
41 40 cvmscbv 
 |-  ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. c e. s ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) } ) = ( a e. J |-> { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " a ) /\ A. v e. b ( A. u e. ( b \ { v } ) ( v i^i u ) = (/) /\ ( F |` v ) e. ( ( C |`t v ) Homeo ( J |`t a ) ) ) ) } )
42 1 2 3 4 5 6 7 8 9 39 41 cvmlift3lem9 
 |-  ( ph -> E. f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) )
43 sconnpconn 
 |-  ( K e. SConn -> K e. PConn )
44 pconnconn 
 |-  ( K e. PConn -> K e. Conn )
45 4 43 44 3syl 
 |-  ( ph -> K e. Conn )
46 pconnconn 
 |-  ( x e. PConn -> x e. Conn )
47 46 ssriv 
 |-  PConn C_ Conn
48 nllyss 
 |-  ( PConn C_ Conn -> N-Locally PConn C_ N-Locally Conn )
49 47 48 ax-mp 
 |-  N-Locally PConn C_ N-Locally Conn
50 49 5 sselid 
 |-  ( ph -> K e. N-Locally Conn )
51 1 2 3 45 50 6 7 8 9 cvmliftmo 
 |-  ( ph -> E* f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) )
52 reu5 
 |-  ( E! f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) <-> ( E. f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ E* f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) ) )
53 42 51 52 sylanbrc 
 |-  ( ph -> E! f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) )