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 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 sseldi
 |-  ( 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 ) )