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