Metamath Proof Explorer

Theorem cvmlift2lem13

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmlift2.b 
|- B = U. C
cvmlift2.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmlift2.g 
|- ( ph -> G e. ( ( II tX II ) Cn J ) )
cvmlift2.p 
|- ( ph -> P e. B )
cvmlift2.i 
|- ( ph -> ( F ` P ) = ( 0 G 0 ) )
cvmlift2.h 
|- H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( f ` 0 ) = P ) )
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 ) )
Assertion cvmlift2lem13 
|- ( ph -> E! g e. ( ( II tX II ) Cn C ) ( ( F o. g ) = G /\ ( 0 g 0 ) = P ) )

Proof

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