Step |
Hyp |
Ref |
Expression |
1 |
|
cvmlift2.b |
|- B = U. C |
2 |
|
cvmlift2.f |
|- ( ph -> F e. ( C CovMap J ) ) |
3 |
|
cvmlift2.g |
|- ( ph -> G e. ( ( II tX II ) Cn J ) ) |
4 |
|
cvmlift2.p |
|- ( ph -> P e. B ) |
5 |
|
cvmlift2.i |
|- ( ph -> ( F ` P ) = ( 0 G 0 ) ) |
6 |
|
cvmlift2.h |
|- H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( f ` 0 ) = P ) ) |
7 |
|
cvmlift2.k |
|- K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) ) |
8 |
|
fveq2 |
|- ( a = z -> ( ( ( II tX II ) CnP C ) ` a ) = ( ( ( II tX II ) CnP C ) ` z ) ) |
9 |
8
|
eleq2d |
|- ( a = z -> ( K e. ( ( ( II tX II ) CnP C ) ` a ) <-> K e. ( ( ( II tX II ) CnP C ) ` z ) ) ) |
10 |
9
|
cbvrabv |
|- { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } = { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) } |
11 |
|
sneq |
|- ( z = b -> { z } = { b } ) |
12 |
11
|
xpeq2d |
|- ( z = b -> ( ( 0 [,] 1 ) X. { z } ) = ( ( 0 [,] 1 ) X. { b } ) ) |
13 |
12
|
sseq1d |
|- ( z = b -> ( ( ( 0 [,] 1 ) X. { z } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( ( 0 [,] 1 ) X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) |
14 |
13
|
cbvrabv |
|- { z e. ( 0 [,] 1 ) | ( ( 0 [,] 1 ) X. { z } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } } = { b e. ( 0 [,] 1 ) | ( ( 0 [,] 1 ) X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } } |
15 |
|
simpr |
|- ( ( c = r /\ d = t ) -> d = t ) |
16 |
15
|
eleq1d |
|- ( ( c = r /\ d = t ) -> ( d e. ( 0 [,] 1 ) <-> t e. ( 0 [,] 1 ) ) ) |
17 |
|
xpeq1 |
|- ( v = u -> ( v X. { b } ) = ( u X. { b } ) ) |
18 |
17
|
sseq1d |
|- ( v = u -> ( ( v X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) |
19 |
|
xpeq1 |
|- ( v = u -> ( v X. { d } ) = ( u X. { d } ) ) |
20 |
19
|
sseq1d |
|- ( v = u -> ( ( v X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) |
21 |
18 20
|
bibi12d |
|- ( v = u -> ( ( ( v X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( v X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) <-> ( ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) ) |
22 |
21
|
cbvrexvw |
|- ( E. v e. ( ( nei ` II ) ` { c } ) ( ( v X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( v X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) <-> E. u e. ( ( nei ` II ) ` { c } ) ( ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) |
23 |
|
simpl |
|- ( ( c = r /\ d = t ) -> c = r ) |
24 |
23
|
sneqd |
|- ( ( c = r /\ d = t ) -> { c } = { r } ) |
25 |
24
|
fveq2d |
|- ( ( c = r /\ d = t ) -> ( ( nei ` II ) ` { c } ) = ( ( nei ` II ) ` { r } ) ) |
26 |
15
|
sneqd |
|- ( ( c = r /\ d = t ) -> { d } = { t } ) |
27 |
26
|
xpeq2d |
|- ( ( c = r /\ d = t ) -> ( u X. { d } ) = ( u X. { t } ) ) |
28 |
27
|
sseq1d |
|- ( ( c = r /\ d = t ) -> ( ( u X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { t } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) |
29 |
28
|
bibi2d |
|- ( ( c = r /\ d = t ) -> ( ( ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) <-> ( ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { t } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) ) |
30 |
25 29
|
rexeqbidv |
|- ( ( c = r /\ d = t ) -> ( E. u e. ( ( nei ` II ) ` { c } ) ( ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) <-> E. u e. ( ( nei ` II ) ` { r } ) ( ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { t } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) ) |
31 |
22 30
|
syl5bb |
|- ( ( c = r /\ d = t ) -> ( E. v e. ( ( nei ` II ) ` { c } ) ( ( v X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( v X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) <-> E. u e. ( ( nei ` II ) ` { r } ) ( ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { t } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) ) |
32 |
16 31
|
anbi12d |
|- ( ( c = r /\ d = t ) -> ( ( d e. ( 0 [,] 1 ) /\ E. v e. ( ( nei ` II ) ` { c } ) ( ( v X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( v X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) <-> ( t e. ( 0 [,] 1 ) /\ E. u e. ( ( nei ` II ) ` { r } ) ( ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { t } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) ) ) |
33 |
32
|
cbvopabv |
|- { <. c , d >. | ( d e. ( 0 [,] 1 ) /\ E. v e. ( ( nei ` II ) ` { c } ) ( ( v X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( v X. { d } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) } = { <. r , t >. | ( t e. ( 0 [,] 1 ) /\ E. u e. ( ( nei ` II ) ` { r } ) ( ( u X. { b } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } <-> ( u X. { t } ) C_ { a e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` a ) } ) ) } |
34 |
1 2 3 4 5 6 7 10 14 33
|
cvmlift2lem12 |
|- ( ph -> K e. ( ( II tX II ) Cn C ) ) |
35 |
1 2 3 4 5 6 7
|
cvmlift2lem7 |
|- ( ph -> ( F o. K ) = G ) |
36 |
|
0elunit |
|- 0 e. ( 0 [,] 1 ) |
37 |
1 2 3 4 5 6 7
|
cvmlift2lem8 |
|- ( ( ph /\ 0 e. ( 0 [,] 1 ) ) -> ( 0 K 0 ) = ( H ` 0 ) ) |
38 |
36 37
|
mpan2 |
|- ( ph -> ( 0 K 0 ) = ( H ` 0 ) ) |
39 |
1 2 3 4 5 6
|
cvmlift2lem2 |
|- ( ph -> ( H e. ( II Cn C ) /\ ( F o. H ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( H ` 0 ) = P ) ) |
40 |
39
|
simp3d |
|- ( ph -> ( H ` 0 ) = P ) |
41 |
38 40
|
eqtrd |
|- ( ph -> ( 0 K 0 ) = P ) |
42 |
|
coeq2 |
|- ( g = K -> ( F o. g ) = ( F o. K ) ) |
43 |
42
|
eqeq1d |
|- ( g = K -> ( ( F o. g ) = G <-> ( F o. K ) = G ) ) |
44 |
|
oveq |
|- ( g = K -> ( 0 g 0 ) = ( 0 K 0 ) ) |
45 |
44
|
eqeq1d |
|- ( g = K -> ( ( 0 g 0 ) = P <-> ( 0 K 0 ) = P ) ) |
46 |
43 45
|
anbi12d |
|- ( g = K -> ( ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) <-> ( ( F o. K ) = G /\ ( 0 K 0 ) = P ) ) ) |
47 |
46
|
rspcev |
|- ( ( K e. ( ( II tX II ) Cn C ) /\ ( ( F o. K ) = G /\ ( 0 K 0 ) = P ) ) -> E. g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) ) |
48 |
34 35 41 47
|
syl12anc |
|- ( ph -> E. g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) ) |
49 |
|
iitop |
|- II e. Top |
50 |
|
iiuni |
|- ( 0 [,] 1 ) = U. II |
51 |
49 49 50 50
|
txunii |
|- ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) = U. ( II tX II ) |
52 |
|
iiconn |
|- II e. Conn |
53 |
|
txconn |
|- ( ( II e. Conn /\ II e. Conn ) -> ( II tX II ) e. Conn ) |
54 |
52 52 53
|
mp2an |
|- ( II tX II ) e. Conn |
55 |
54
|
a1i |
|- ( ph -> ( II tX II ) e. Conn ) |
56 |
|
iinllyconn |
|- II e. N-Locally Conn |
57 |
|
txconn |
|- ( ( x e. Conn /\ y e. Conn ) -> ( x tX y ) e. Conn ) |
58 |
57
|
txnlly |
|- ( ( II e. N-Locally Conn /\ II e. N-Locally Conn ) -> ( II tX II ) e. N-Locally Conn ) |
59 |
56 56 58
|
mp2an |
|- ( II tX II ) e. N-Locally Conn |
60 |
59
|
a1i |
|- ( ph -> ( II tX II ) e. N-Locally Conn ) |
61 |
|
opelxpi |
|- ( ( 0 e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) -> <. 0 , 0 >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) |
62 |
36 36 61
|
mp2an |
|- <. 0 , 0 >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) |
63 |
62
|
a1i |
|- ( ph -> <. 0 , 0 >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) |
64 |
|
df-ov |
|- ( 0 G 0 ) = ( G ` <. 0 , 0 >. ) |
65 |
5 64
|
eqtrdi |
|- ( ph -> ( F ` P ) = ( G ` <. 0 , 0 >. ) ) |
66 |
1 51 2 55 60 63 3 4 65
|
cvmliftmo |
|- ( ph -> E* g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( g ` <. 0 , 0 >. ) = P ) ) |
67 |
|
df-ov |
|- ( 0 g 0 ) = ( g ` <. 0 , 0 >. ) |
68 |
67
|
eqeq1i |
|- ( ( 0 g 0 ) = P <-> ( g ` <. 0 , 0 >. ) = P ) |
69 |
68
|
anbi2i |
|- ( ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) <-> ( ( F o. g ) = G /\ ( g ` <. 0 , 0 >. ) = P ) ) |
70 |
69
|
rmobii |
|- ( E* g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) <-> E* g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( g ` <. 0 , 0 >. ) = P ) ) |
71 |
66 70
|
sylibr |
|- ( ph -> E* g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) ) |
72 |
|
reu5 |
|- ( E! g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) <-> ( E. g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) /\ E* g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) ) ) |
73 |
48 71 72
|
sylanbrc |
|- ( ph -> E! g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) ) |