Metamath Proof Explorer

Theorem cvmliftlem15

Description: Lemma for cvmlift . Discharge the assumptions of cvmliftlem14 . The set of all open subsets u of the unit interval such that G " u is contained in an even covering of some open set in J is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii , there is a subdivision of the closed unit interval into N equal parts such that each part is entirely contained within one such open set of J . Then using finite choice ac6sfi to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 . (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 
|- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
cvmliftlem.b 
|- B = U. C
cvmliftlem.x 
|- X = U. J
cvmliftlem.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmliftlem.g 
|- ( ph -> G e. ( II Cn J ) )
cvmliftlem.p 
|- ( ph -> P e. B )
cvmliftlem.e 
|- ( ph -> ( F ` P ) = ( G ` 0 ) )
Assertion cvmliftlem15 
|- ( ph -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2 cvmliftlem.b 
 |-  B = U. C
3 cvmliftlem.x 
 |-  X = U. J
4 cvmliftlem.f 
 |-  ( ph -> F e. ( C CovMap J ) )
5 cvmliftlem.g 
 |-  ( ph -> G e. ( II Cn J ) )
6 cvmliftlem.p 
 |-  ( ph -> P e. B )
7 cvmliftlem.e 
 |-  ( ph -> ( F ` P ) = ( G ` 0 ) )
8 ssrab2 
 |-  { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } C_ II
9 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> G e. ( II Cn J ) )
10 simprl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> j e. J )
11 cnima 
 |-  ( ( G e. ( II Cn J ) /\ j e. J ) -> ( `' G " j ) e. II )
12 9 10 11 syl2anc 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> ( `' G " j ) e. II )
13 simplr 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> x e. ( 0 [,] 1 ) )
14 simprrl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> ( G ` x ) e. j )
15 iiuni 
 |-  ( 0 [,] 1 ) = U. II
16 15 3 cnf 
 |-  ( G e. ( II Cn J ) -> G : ( 0 [,] 1 ) --> X )
17 5 16 syl 
 |-  ( ph -> G : ( 0 [,] 1 ) --> X )
18 17 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> G : ( 0 [,] 1 ) --> X )
19 ffn 
 |-  ( G : ( 0 [,] 1 ) --> X -> G Fn ( 0 [,] 1 ) )
20 elpreima 
 |-  ( G Fn ( 0 [,] 1 ) -> ( x e. ( `' G " j ) <-> ( x e. ( 0 [,] 1 ) /\ ( G ` x ) e. j ) ) )
21 18 19 20 3syl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> ( x e. ( `' G " j ) <-> ( x e. ( 0 [,] 1 ) /\ ( G ` x ) e. j ) ) )
22 13 14 21 mpbir2and 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> x e. ( `' G " j ) )
23 simprrr 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> ( S ` j ) =/= (/) )
24 ffun 
 |-  ( G : ( 0 [,] 1 ) --> X -> Fun G )
25 funimacnv 
 |-  ( Fun G -> ( G " ( `' G " j ) ) = ( j i^i ran G ) )
26 18 24 25 3syl 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> ( G " ( `' G " j ) ) = ( j i^i ran G ) )
27 inss1 
 |-  ( j i^i ran G ) C_ j
28 26 27 eqsstrdi 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> ( G " ( `' G " j ) ) C_ j )
29 28 ralrimivw 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> A. s e. ( S ` j ) ( G " ( `' G " j ) ) C_ j )
30 r19.2z 
 |-  ( ( ( S ` j ) =/= (/) /\ A. s e. ( S ` j ) ( G " ( `' G " j ) ) C_ j ) -> E. s e. ( S ` j ) ( G " ( `' G " j ) ) C_ j )
31 23 29 30 syl2anc 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> E. s e. ( S ` j ) ( G " ( `' G " j ) ) C_ j )
32 eleq2 
 |-  ( u = ( `' G " j ) -> ( x e. u <-> x e. ( `' G " j ) ) )
33 imaeq2 
 |-  ( u = ( `' G " j ) -> ( G " u ) = ( G " ( `' G " j ) ) )
34 33 sseq1d 
 |-  ( u = ( `' G " j ) -> ( ( G " u ) C_ j <-> ( G " ( `' G " j ) ) C_ j ) )
35 34 rexbidv 
 |-  ( u = ( `' G " j ) -> ( E. s e. ( S ` j ) ( G " u ) C_ j <-> E. s e. ( S ` j ) ( G " ( `' G " j ) ) C_ j ) )
36 32 35 anbi12d 
 |-  ( u = ( `' G " j ) -> ( ( x e. u /\ E. s e. ( S ` j ) ( G " u ) C_ j ) <-> ( x e. ( `' G " j ) /\ E. s e. ( S ` j ) ( G " ( `' G " j ) ) C_ j ) ) )
37 36 rspcev 
 |-  ( ( ( `' G " j ) e. II /\ ( x e. ( `' G " j ) /\ E. s e. ( S ` j ) ( G " ( `' G " j ) ) C_ j ) ) -> E. u e. II ( x e. u /\ E. s e. ( S ` j ) ( G " u ) C_ j ) )
38 12 22 31 37 syl12anc 
 |-  ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ ( j e. J /\ ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) ) ) -> E. u e. II ( x e. u /\ E. s e. ( S ` j ) ( G " u ) C_ j ) )
39 4 adantr 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> F e. ( C CovMap J ) )
40 17 ffvelcdmda 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> ( G ` x ) e. X )
41 1 3 cvmcov 
 |-  ( ( F e. ( C CovMap J ) /\ ( G ` x ) e. X ) -> E. j e. J ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) )
42 39 40 41 syl2anc 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> E. j e. J ( ( G ` x ) e. j /\ ( S ` j ) =/= (/) ) )
43 38 42 reximddv 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> E. j e. J E. u e. II ( x e. u /\ E. s e. ( S ` j ) ( G " u ) C_ j ) )
44 r19.42v 
 |-  ( E. j e. J ( x e. u /\ E. s e. ( S ` j ) ( G " u ) C_ j ) <-> ( x e. u /\ E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j ) )
45 44 rexbii 
 |-  ( E. u e. II E. j e. J ( x e. u /\ E. s e. ( S ` j ) ( G " u ) C_ j ) <-> E. u e. II ( x e. u /\ E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j ) )
46 rexcom 
 |-  ( E. j e. J E. u e. II ( x e. u /\ E. s e. ( S ` j ) ( G " u ) C_ j ) <-> E. u e. II E. j e. J ( x e. u /\ E. s e. ( S ` j ) ( G " u ) C_ j ) )
47 elunirab 
 |-  ( x e. U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } <-> E. u e. II ( x e. u /\ E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j ) )
48 45 46 47 3bitr4i 
 |-  ( E. j e. J E. u e. II ( x e. u /\ E. s e. ( S ` j ) ( G " u ) C_ j ) <-> x e. U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } )
49 43 48 sylib 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> x e. U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } )
50 49 ex 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) -> x e. U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ) )
51 50 ssrdv 
 |-  ( ph -> ( 0 [,] 1 ) C_ U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } )
52 uniss 
 |-  ( { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } C_ II -> U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } C_ U. II )
53 8 52 mp1i 
 |-  ( ph -> U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } C_ U. II )
54 53 15 sseqtrrdi 
 |-  ( ph -> U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } C_ ( 0 [,] 1 ) )
55 51 54 eqssd 
 |-  ( ph -> ( 0 [,] 1 ) = U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } )
56 lebnumii 
 |-  ( ( { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } C_ II /\ ( 0 [,] 1 ) = U. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ) -> E. n e. NN A. k e. ( 1 ... n ) E. v e. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v )
57 8 55 56 sylancr 
 |-  ( ph -> E. n e. NN A. k e. ( 1 ... n ) E. v e. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v )
58 fzfi 
 |-  ( 1 ... n ) e. Fin
59 imaeq2 
 |-  ( u = v -> ( G " u ) = ( G " v ) )
60 59 sseq1d 
 |-  ( u = v -> ( ( G " u ) C_ j <-> ( G " v ) C_ j ) )
61 60 2rexbidv 
 |-  ( u = v -> ( E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j <-> E. j e. J E. s e. ( S ` j ) ( G " v ) C_ j ) )
62 61 rexrab 
 |-  ( E. v e. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v <-> E. v e. II ( E. j e. J E. s e. ( S ` j ) ( G " v ) C_ j /\ ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v ) )
63 vex 
 |-  j e. _V
64 vex 
 |-  s e. _V
65 63 64 op1std 
 |-  ( u = <. j , s >. -> ( 1st ` u ) = j )
66 65 sseq2d 
 |-  ( u = <. j , s >. -> ( ( G " v ) C_ ( 1st ` u ) <-> ( G " v ) C_ j ) )
67 66 rexiunxp 
 |-  ( E. u e. U_ j e. J ( { j } X. ( S ` j ) ) ( G " v ) C_ ( 1st ` u ) <-> E. j e. J E. s e. ( S ` j ) ( G " v ) C_ j )
68 imass2 
 |-  ( ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v -> ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( G " v ) )
69 sstr2 
 |-  ( ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( G " v ) -> ( ( G " v ) C_ ( 1st ` u ) -> ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) ) )
70 68 69 syl 
 |-  ( ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v -> ( ( G " v ) C_ ( 1st ` u ) -> ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) ) )
71 70 reximdv 
 |-  ( ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v -> ( E. u e. U_ j e. J ( { j } X. ( S ` j ) ) ( G " v ) C_ ( 1st ` u ) -> E. u e. U_ j e. J ( { j } X. ( S ` j ) ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) ) )
72 67 71 biimtrrid 
 |-  ( ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v -> ( E. j e. J E. s e. ( S ` j ) ( G " v ) C_ j -> E. u e. U_ j e. J ( { j } X. ( S ` j ) ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) ) )
73 72 impcom 
 |-  ( ( E. j e. J E. s e. ( S ` j ) ( G " v ) C_ j /\ ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v ) -> E. u e. U_ j e. J ( { j } X. ( S ` j ) ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) )
74 73 rexlimivw 
 |-  ( E. v e. II ( E. j e. J E. s e. ( S ` j ) ( G " v ) C_ j /\ ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v ) -> E. u e. U_ j e. J ( { j } X. ( S ` j ) ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) )
75 62 74 sylbi 
 |-  ( E. v e. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v -> E. u e. U_ j e. J ( { j } X. ( S ` j ) ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) )
76 75 ralimi 
 |-  ( A. k e. ( 1 ... n ) E. v e. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v -> A. k e. ( 1 ... n ) E. u e. U_ j e. J ( { j } X. ( S ` j ) ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) )
77 fveq2 
 |-  ( u = ( g ` k ) -> ( 1st ` u ) = ( 1st ` ( g ` k ) ) )
78 77 sseq2d 
 |-  ( u = ( g ` k ) -> ( ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) <-> ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) )
79 78 ac6sfi 
 |-  ( ( ( 1 ... n ) e. Fin /\ A. k e. ( 1 ... n ) E. u e. U_ j e. J ( { j } X. ( S ` j ) ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` u ) ) -> E. g ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) )
80 58 76 79 sylancr 
 |-  ( A. k e. ( 1 ... n ) E. v e. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v -> E. g ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) )
81 4 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) ) -> F e. ( C CovMap J ) )
82 5 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) ) -> G e. ( II Cn J ) )
83 6 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) ) -> P e. B )
84 7 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) ) -> ( F ` P ) = ( G ` 0 ) )
85 simplr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) ) -> n e. NN )
86 simprl 
 |-  ( ( ( ph /\ n e. NN ) /\ ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) ) -> g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
87 sneq 
 |-  ( j = a -> { j } = { a } )
88 fveq2 
 |-  ( j = a -> ( S ` j ) = ( S ` a ) )
89 87 88 xpeq12d 
 |-  ( j = a -> ( { j } X. ( S ` j ) ) = ( { a } X. ( S ` a ) ) )
90 89 cbviunv 
 |-  U_ j e. J ( { j } X. ( S ` j ) ) = U_ a e. J ( { a } X. ( S ` a ) )
91 feq3 
 |-  ( U_ j e. J ( { j } X. ( S ` j ) ) = U_ a e. J ( { a } X. ( S ` a ) ) -> ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) <-> g : ( 1 ... n ) --> U_ a e. J ( { a } X. ( S ` a ) ) ) )
92 90 91 ax-mp 
 |-  ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) <-> g : ( 1 ... n ) --> U_ a e. J ( { a } X. ( S ` a ) ) )
93 86 92 sylib 
 |-  ( ( ( ph /\ n e. NN ) /\ ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) ) -> g : ( 1 ... n ) --> U_ a e. J ( { a } X. ( S ` a ) ) )
94 simprr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) ) -> A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) )
95 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
96 2fveq3 
 |-  ( t = z -> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` t ) ) = ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` z ) ) )
97 96 cbvmptv 
 |-  ( t e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` t ) ) ) = ( z e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` z ) ) )
98 eleq2 
 |-  ( c = b -> ( ( y ` ( ( w - 1 ) / n ) ) e. c <-> ( y ` ( ( w - 1 ) / n ) ) e. b ) )
99 98 cbvriotavw 
 |-  ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) = ( iota_ b e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. b )
100 fveq1 
 |-  ( y = x -> ( y ` ( ( w - 1 ) / n ) ) = ( x ` ( ( w - 1 ) / n ) ) )
101 100 eleq1d 
 |-  ( y = x -> ( ( y ` ( ( w - 1 ) / n ) ) e. b <-> ( x ` ( ( w - 1 ) / n ) ) e. b ) )
102 101 riotabidv 
 |-  ( y = x -> ( iota_ b e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. b ) = ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) )
103 99 102 eqtrid 
 |-  ( y = x -> ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) = ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) )
104 103 reseq2d 
 |-  ( y = x -> ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) = ( F |` ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) ) )
105 104 cnveqd 
 |-  ( y = x -> `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) = `' ( F |` ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) ) )
106 105 fveq1d 
 |-  ( y = x -> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` z ) ) = ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) )
107 106 mpteq2dv 
 |-  ( y = x -> ( z e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` z ) ) ) = ( z e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) ) )
108 97 107 eqtrid 
 |-  ( y = x -> ( t e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` t ) ) ) = ( z e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) ) )
109 oveq1 
 |-  ( w = m -> ( w - 1 ) = ( m - 1 ) )
110 109 oveq1d 
 |-  ( w = m -> ( ( w - 1 ) / n ) = ( ( m - 1 ) / n ) )
111 oveq1 
 |-  ( w = m -> ( w / n ) = ( m / n ) )
112 110 111 oveq12d 
 |-  ( w = m -> ( ( ( w - 1 ) / n ) [,] ( w / n ) ) = ( ( ( m - 1 ) / n ) [,] ( m / n ) ) )
113 2fveq3 
 |-  ( w = m -> ( 2nd ` ( g ` w ) ) = ( 2nd ` ( g ` m ) ) )
114 110 fveq2d 
 |-  ( w = m -> ( x ` ( ( w - 1 ) / n ) ) = ( x ` ( ( m - 1 ) / n ) ) )
115 114 eleq1d 
 |-  ( w = m -> ( ( x ` ( ( w - 1 ) / n ) ) e. b <-> ( x ` ( ( m - 1 ) / n ) ) e. b ) )
116 113 115 riotaeqbidv 
 |-  ( w = m -> ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) = ( iota_ b e. ( 2nd ` ( g ` m ) ) ( x ` ( ( m - 1 ) / n ) ) e. b ) )
117 116 reseq2d 
 |-  ( w = m -> ( F |` ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) ) = ( F |` ( iota_ b e. ( 2nd ` ( g ` m ) ) ( x ` ( ( m - 1 ) / n ) ) e. b ) ) )
118 117 cnveqd 
 |-  ( w = m -> `' ( F |` ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) ) = `' ( F |` ( iota_ b e. ( 2nd ` ( g ` m ) ) ( x ` ( ( m - 1 ) / n ) ) e. b ) ) )
119 118 fveq1d 
 |-  ( w = m -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) = ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` m ) ) ( x ` ( ( m - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) )
120 112 119 mpteq12dv 
 |-  ( w = m -> ( z e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` w ) ) ( x ` ( ( w - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) ) = ( z e. ( ( ( m - 1 ) / n ) [,] ( m / n ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` m ) ) ( x ` ( ( m - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) ) )
121 108 120 cbvmpov 
 |-  ( y e. _V , w e. NN |-> ( t e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` t ) ) ) ) = ( x e. _V , m e. NN |-> ( z e. ( ( ( m - 1 ) / n ) [,] ( m / n ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` m ) ) ( x ` ( ( m - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) ) )
122 seqeq2 
 |-  ( ( y e. _V , w e. NN |-> ( t e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` t ) ) ) ) = ( x e. _V , m e. NN |-> ( z e. ( ( ( m - 1 ) / n ) [,] ( m / n ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` m ) ) ( x ` ( ( m - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) ) ) -> seq 0 ( ( y e. _V , w e. NN |-> ( t e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` t ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ) = seq 0 ( ( x e. _V , m e. NN |-> ( z e. ( ( ( m - 1 ) / n ) [,] ( m / n ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` m ) ) ( x ` ( ( m - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ) )
123 121 122 ax-mp 
 |-  seq 0 ( ( y e. _V , w e. NN |-> ( t e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` t ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ) = seq 0 ( ( x e. _V , m e. NN |-> ( z e. ( ( ( m - 1 ) / n ) [,] ( m / n ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( g ` m ) ) ( x ` ( ( m - 1 ) / n ) ) e. b ) ) ` ( G ` z ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) )
124 eqid 
 |-  U_ k e. ( 1 ... n ) ( seq 0 ( ( y e. _V , w e. NN |-> ( t e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` t ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ) ` k ) = U_ k e. ( 1 ... n ) ( seq 0 ( ( y e. _V , w e. NN |-> ( t e. ( ( ( w - 1 ) / n ) [,] ( w / n ) ) |-> ( `' ( F |` ( iota_ c e. ( 2nd ` ( g ` w ) ) ( y ` ( ( w - 1 ) / n ) ) e. c ) ) ` ( G ` t ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ) ` k )
125 1 2 3 81 82 83 84 85 93 94 95 123 124 cvmliftlem14 
 |-  ( ( ( ph /\ n e. NN ) /\ ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) ) -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )
126 125 ex 
 |-  ( ( ph /\ n e. NN ) -> ( ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) ) )
127 126 exlimdv 
 |-  ( ( ph /\ n e. NN ) -> ( E. g ( g : ( 1 ... n ) --> U_ j e. J ( { j } X. ( S ` j ) ) /\ A. k e. ( 1 ... n ) ( G " ( ( ( k - 1 ) / n ) [,] ( k / n ) ) ) C_ ( 1st ` ( g ` k ) ) ) -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) ) )
128 80 127 syl5 
 |-  ( ( ph /\ n e. NN ) -> ( A. k e. ( 1 ... n ) E. v e. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) ) )
129 128 rexlimdva 
 |-  ( ph -> ( E. n e. NN A. k e. ( 1 ... n ) E. v e. { u e. II | E. j e. J E. s e. ( S ` j ) ( G " u ) C_ j } ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ v -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) ) )
130 57 129 mpd 
 |-  ( ph -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )