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 ffvelrnda
 |-  ( ( 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 syl5bir
 |-  ( ( ( ( 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 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 ) )