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 ) ) |