Metamath Proof Explorer

Theorem cvmlift2lem10

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-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 ) )
cvmlift2lem10.s 
|- S = ( 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 ) ) ) ) } )
cvmlift2lem10.1 
|- ( ph -> X e. ( 0 [,] 1 ) )
cvmlift2lem10.2 
|- ( ph -> Y e. ( 0 [,] 1 ) )
Assertion cvmlift2lem10 
|- ( ph -> E. u e. II E. v e. II ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) )

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 cvmlift2lem10.s 
 |-  S = ( 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 ) ) ) ) } )
9 cvmlift2lem10.1 
 |-  ( ph -> X e. ( 0 [,] 1 ) )
10 cvmlift2lem10.2 
 |-  ( ph -> Y e. ( 0 [,] 1 ) )
11 iitop 
 |-  II e. Top
12 iiuni 
 |-  ( 0 [,] 1 ) = U. II
13 11 11 12 12 txunii 
 |-  ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) = U. ( II tX II )
14 eqid 
 |-  U. J = U. J
15 13 14 cnf 
 |-  ( G e. ( ( II tX II ) Cn J ) -> G : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> U. J )
16 3 15 syl 
 |-  ( ph -> G : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> U. J )
17 9 10 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
18 16 17 ffvelcdmd 
 |-  ( ph -> ( G ` <. X , Y >. ) e. U. J )
19 8 14 cvmcov 
 |-  ( ( F e. ( C CovMap J ) /\ ( G ` <. X , Y >. ) e. U. J ) -> E. m e. J ( ( G ` <. X , Y >. ) e. m /\ ( S ` m ) =/= (/) ) )
20 2 18 19 syl2anc 
 |-  ( ph -> E. m e. J ( ( G ` <. X , Y >. ) e. m /\ ( S ` m ) =/= (/) ) )
21 n0 
 |-  ( ( S ` m ) =/= (/) <-> E. t t e. ( S ` m ) )
22 eleq1 
 |-  ( z = <. X , Y >. -> ( z e. ( a X. b ) <-> <. X , Y >. e. ( a X. b ) ) )
23 opelxp 
 |-  ( <. X , Y >. e. ( a X. b ) <-> ( X e. a /\ Y e. b ) )
24 22 23 bitrdi 
 |-  ( z = <. X , Y >. -> ( z e. ( a X. b ) <-> ( X e. a /\ Y e. b ) ) )
25 24 anbi1d 
 |-  ( z = <. X , Y >. -> ( ( z e. ( a X. b ) /\ ( a X. b ) C_ ( `' G " m ) ) <-> ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) )
26 25 2rexbidv 
 |-  ( z = <. X , Y >. -> ( E. a e. II E. b e. II ( z e. ( a X. b ) /\ ( a X. b ) C_ ( `' G " m ) ) <-> E. a e. II E. b e. II ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) )
27 3 adantr 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> G e. ( ( II tX II ) Cn J ) )
28 8 cvmsrcl 
 |-  ( t e. ( S ` m ) -> m e. J )
29 28 ad2antll 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> m e. J )
30 cnima 
 |-  ( ( G e. ( ( II tX II ) Cn J ) /\ m e. J ) -> ( `' G " m ) e. ( II tX II ) )
31 27 29 30 syl2anc 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> ( `' G " m ) e. ( II tX II ) )
32 eltx 
 |-  ( ( II e. Top /\ II e. Top ) -> ( ( `' G " m ) e. ( II tX II ) <-> A. z e. ( `' G " m ) E. a e. II E. b e. II ( z e. ( a X. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) )
33 11 11 32 mp2an 
 |-  ( ( `' G " m ) e. ( II tX II ) <-> A. z e. ( `' G " m ) E. a e. II E. b e. II ( z e. ( a X. b ) /\ ( a X. b ) C_ ( `' G " m ) ) )
34 31 33 sylib 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> A. z e. ( `' G " m ) E. a e. II E. b e. II ( z e. ( a X. b ) /\ ( a X. b ) C_ ( `' G " m ) ) )
35 17 adantr 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> <. X , Y >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
36 simprl 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> ( G ` <. X , Y >. ) e. m )
37 16 adantr 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> G : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> U. J )
38 ffn 
 |-  ( G : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> U. J -> G Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
39 elpreima 
 |-  ( G Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) -> ( <. X , Y >. e. ( `' G " m ) <-> ( <. X , Y >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) /\ ( G ` <. X , Y >. ) e. m ) ) )
40 37 38 39 3syl 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> ( <. X , Y >. e. ( `' G " m ) <-> ( <. X , Y >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) /\ ( G ` <. X , Y >. ) e. m ) ) )
41 35 36 40 mpbir2and 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> <. X , Y >. e. ( `' G " m ) )
42 26 34 41 rspcdva 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> E. a e. II E. b e. II ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) )
43 iillysconn 
 |-  II e. Locally SConn
44 simplrl 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> a e. II )
45 simprll 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> X e. a )
46 llyi 
 |-  ( ( II e. Locally SConn /\ a e. II /\ X e. a ) -> E. u e. II ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) )
47 43 44 45 46 mp3an2i 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> E. u e. II ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) )
48 simplrr 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> b e. II )
49 simprlr 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> Y e. b )
50 llyi 
 |-  ( ( II e. Locally SConn /\ b e. II /\ Y e. b ) -> E. v e. II ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) )
51 43 48 49 50 mp3an2i 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> E. v e. II ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) )
52 reeanv 
 |-  ( E. u e. II E. v e. II ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) <-> ( E. u e. II ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ E. v e. II ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) )
53 simpl2 
 |-  ( ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> X e. u )
54 53 a1i 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> ( ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> X e. u ) )
55 simpr2 
 |-  ( ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> Y e. v )
56 55 a1i 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> ( ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> Y e. v ) )
57 simprl1 
 |-  ( ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) /\ ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) ) -> u C_ a )
58 simprr1 
 |-  ( ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) /\ ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) ) -> v C_ b )
59 xpss12 
 |-  ( ( u C_ a /\ v C_ b ) -> ( u X. v ) C_ ( a X. b ) )
60 57 58 59 syl2anc 
 |-  ( ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) /\ ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) ) -> ( u X. v ) C_ ( a X. b ) )
61 simplrr 
 |-  ( ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) /\ ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) ) -> ( a X. b ) C_ ( `' G " m ) )
62 60 61 sstrd 
 |-  ( ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) /\ ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) ) -> ( u X. v ) C_ ( `' G " m ) )
63 62 ex 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> ( ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> ( u X. v ) C_ ( `' G " m ) ) )
64 54 56 63 3jcad 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> ( ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) ) )
65 simp3 
 |-  ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) -> ( II |`t u ) e. SConn )
66 simp3 
 |-  ( ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) -> ( II |`t v ) e. SConn )
67 65 66 anim12i 
 |-  ( ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) )
68 64 67 jca2 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> ( ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) )
69 68 reximdv 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> ( E. v e. II ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> E. v e. II ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) )
70 69 reximdv 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> ( E. u e. II E. v e. II ( ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> E. u e. II E. v e. II ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) )
71 52 70 biimtrrid 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> ( ( E. u e. II ( u C_ a /\ X e. u /\ ( II |`t u ) e. SConn ) /\ E. v e. II ( v C_ b /\ Y e. v /\ ( II |`t v ) e. SConn ) ) -> E. u e. II E. v e. II ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) )
72 47 51 71 mp2and 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) /\ ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) ) -> E. u e. II E. v e. II ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) )
73 72 ex 
 |-  ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( a e. II /\ b e. II ) ) -> ( ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) -> E. u e. II E. v e. II ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) )
74 73 rexlimdvva 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> ( E. a e. II E. b e. II ( ( X e. a /\ Y e. b ) /\ ( a X. b ) C_ ( `' G " m ) ) -> E. u e. II E. v e. II ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) )
75 42 74 mpd 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> E. u e. II E. v e. II ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) )
76 simp3l1 
 |-  ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) -> X e. u )
77 simp3l2 
 |-  ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) -> Y e. v )
78 simpl1l 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ph )
79 78 2 syl 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> F e. ( C CovMap J ) )
80 78 3 syl 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> G e. ( ( II tX II ) Cn J ) )
81 78 4 syl 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> P e. B )
82 78 5 syl 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( F ` P ) = ( 0 G 0 ) )
83 df-ov 
 |-  ( X G Y ) = ( G ` <. X , Y >. )
84 simpl1r 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) )
85 84 simpld 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( G ` <. X , Y >. ) e. m )
86 83 85 eqeltrid 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( X G Y ) e. m )
87 84 simprd 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> t e. ( S ` m ) )
88 simpl2l 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> u e. II )
89 simpl2r 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> v e. II )
90 simp3rl 
 |-  ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) -> ( II |`t u ) e. SConn )
91 90 adantr 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( II |`t u ) e. SConn )
92 sconnpconn 
 |-  ( ( II |`t u ) e. SConn -> ( II |`t u ) e. PConn )
93 pconnconn 
 |-  ( ( II |`t u ) e. PConn -> ( II |`t u ) e. Conn )
94 91 92 93 3syl 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( II |`t u ) e. Conn )
95 simp3rr 
 |-  ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) -> ( II |`t v ) e. SConn )
96 95 adantr 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( II |`t v ) e. SConn )
97 sconnpconn 
 |-  ( ( II |`t v ) e. SConn -> ( II |`t v ) e. PConn )
98 pconnconn 
 |-  ( ( II |`t v ) e. PConn -> ( II |`t v ) e. Conn )
99 96 97 98 3syl 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( II |`t v ) e. Conn )
100 76 adantr 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> X e. u )
101 77 adantr 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> Y e. v )
102 simp3l3 
 |-  ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) -> ( u X. v ) C_ ( `' G " m ) )
103 102 adantr 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( u X. v ) C_ ( `' G " m ) )
104 simprl 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> w e. v )
105 simprr 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) )
106 eqid 
 |-  ( iota_ b e. t ( X K Y ) e. b ) = ( iota_ b e. t ( X K Y ) e. b )
107 1 79 80 81 82 6 7 8 86 87 88 89 94 99 100 101 103 104 105 106 cvmlift2lem9 
 |-  ( ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) /\ ( w e. v /\ ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) ) ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) )
108 107 rexlimdvaa 
 |-  ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) -> ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) )
109 76 77 108 3jca 
 |-  ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) /\ ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) ) -> ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) )
110 109 3expia 
 |-  ( ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) /\ ( u e. II /\ v e. II ) ) -> ( ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) -> ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) ) )
111 110 reximdvva 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> ( E. u e. II E. v e. II ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' G " m ) ) /\ ( ( II |`t u ) e. SConn /\ ( II |`t v ) e. SConn ) ) -> E. u e. II E. v e. II ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) ) )
112 75 111 mpd 
 |-  ( ( ph /\ ( ( G ` <. X , Y >. ) e. m /\ t e. ( S ` m ) ) ) -> E. u e. II E. v e. II ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) )
113 112 expr 
 |-  ( ( ph /\ ( G ` <. X , Y >. ) e. m ) -> ( t e. ( S ` m ) -> E. u e. II E. v e. II ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) ) )
114 113 exlimdv 
 |-  ( ( ph /\ ( G ` <. X , Y >. ) e. m ) -> ( E. t t e. ( S ` m ) -> E. u e. II E. v e. II ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) ) )
115 21 114 biimtrid 
 |-  ( ( ph /\ ( G ` <. X , Y >. ) e. m ) -> ( ( S ` m ) =/= (/) -> E. u e. II E. v e. II ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) ) )
116 115 expimpd 
 |-  ( ph -> ( ( ( G ` <. X , Y >. ) e. m /\ ( S ` m ) =/= (/) ) -> E. u e. II E. v e. II ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) ) )
117 116 rexlimdvw 
 |-  ( ph -> ( E. m e. J ( ( G ` <. X , Y >. ) e. m /\ ( S ` m ) =/= (/) ) -> E. u e. II E. v e. II ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) ) )
118 20 117 mpd 
 |-  ( ph -> E. u e. II E. v e. II ( X e. u /\ Y e. v /\ ( E. w e. v ( K |` ( u X. { w } ) ) e. ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) -> ( K |` ( u X. v ) ) e. ( ( ( II tX II ) |`t ( u X. v ) ) Cn C ) ) ) )