Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftphtlem Structured version   Unicode version

Theorem cvmliftphtlem 27120
Description: Lemma for cvmliftpht 27121. (Contributed by Mario Carneiro, 6-Jul-2015.)
Hypotheses
Ref Expression
cvmliftpht.b  |-  B  = 
U. C
cvmliftpht.m  |-  M  =  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f ` 
0 )  =  P ) )
cvmliftpht.n  |-  N  =  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  H  /\  ( f ` 
0 )  =  P ) )
cvmliftpht.f  |-  ( ph  ->  F  e.  ( C CovMap  J ) )
cvmliftpht.p  |-  ( ph  ->  P  e.  B )
cvmliftpht.e  |-  ( ph  ->  ( F `  P
)  =  ( G `
 0 ) )
cvmliftphtlem.g  |-  ( ph  ->  G  e.  ( II 
Cn  J ) )
cvmliftphtlem.h  |-  ( ph  ->  H  e.  ( II 
Cn  J ) )
cvmliftphtlem.k  |-  ( ph  ->  K  e.  ( G ( PHtpy `  J ) H ) )
cvmliftphtlem.a  |-  ( ph  ->  A  e.  ( ( II  tX  II )  Cn  C ) )
cvmliftphtlem.c  |-  ( ph  ->  ( F  o.  A
)  =  K )
cvmliftphtlem.0  |-  ( ph  ->  ( 0 A 0 )  =  P )
Assertion
Ref Expression
cvmliftphtlem  |-  ( ph  ->  A  e.  ( M ( PHtpy `  C ) N ) )
Distinct variable groups:    A, f    B, f    f, F    f, J    C, f    f, G   
f, H    P, f
Allowed substitution hints:    ph( f)    K( f)    M( f)    N( f)

Proof of Theorem cvmliftphtlem
Dummy variables  s  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmliftpht.b . . . 4  |-  B  = 
U. C
2 cvmliftpht.m . . . 4  |-  M  =  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f ` 
0 )  =  P ) )
3 cvmliftpht.f . . . 4  |-  ( ph  ->  F  e.  ( C CovMap  J ) )
4 cvmliftphtlem.g . . . 4  |-  ( ph  ->  G  e.  ( II 
Cn  J ) )
5 cvmliftpht.p . . . 4  |-  ( ph  ->  P  e.  B )
6 cvmliftpht.e . . . 4  |-  ( ph  ->  ( F `  P
)  =  ( G `
 0 ) )
71, 2, 3, 4, 5, 6cvmliftiota 27104 . . 3  |-  ( ph  ->  ( M  e.  ( II  Cn  C )  /\  ( F  o.  M )  =  G  /\  ( M ` 
0 )  =  P ) )
87simp1d 995 . 2  |-  ( ph  ->  M  e.  ( II 
Cn  C ) )
9 cvmliftpht.n . . . 4  |-  N  =  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  H  /\  ( f ` 
0 )  =  P ) )
10 cvmliftphtlem.h . . . 4  |-  ( ph  ->  H  e.  ( II 
Cn  J ) )
11 cvmliftphtlem.k . . . . . . 7  |-  ( ph  ->  K  e.  ( G ( PHtpy `  J ) H ) )
124, 10, 11phtpy01 20457 . . . . . 6  |-  ( ph  ->  ( ( G ` 
0 )  =  ( H `  0 )  /\  ( G ` 
1 )  =  ( H `  1 ) ) )
1312simpld 456 . . . . 5  |-  ( ph  ->  ( G `  0
)  =  ( H `
 0 ) )
146, 13eqtrd 2473 . . . 4  |-  ( ph  ->  ( F `  P
)  =  ( H `
 0 ) )
151, 9, 3, 10, 5, 14cvmliftiota 27104 . . 3  |-  ( ph  ->  ( N  e.  ( II  Cn  C )  /\  ( F  o.  N )  =  H  /\  ( N ` 
0 )  =  P ) )
1615simp1d 995 . 2  |-  ( ph  ->  N  e.  ( II 
Cn  C ) )
17 cvmliftphtlem.a . 2  |-  ( ph  ->  A  e.  ( ( II  tX  II )  Cn  C ) )
18 iitop 20356 . . . . . . . . . . . . . . . 16  |-  II  e.  Top
19 iiuni 20357 . . . . . . . . . . . . . . . 16  |-  ( 0 [,] 1 )  = 
U. II
2018, 18, 19, 19txunii 19066 . . . . . . . . . . . . . . 15  |-  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )  = 
U. ( II  tX  II )
2120, 1cnf 18750 . . . . . . . . . . . . . 14  |-  ( A  e.  ( ( II 
tX  II )  Cn  C )  ->  A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) --> B )
2217, 21syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B )
23 0elunit 11399 . . . . . . . . . . . . . 14  |-  0  e.  ( 0 [,] 1
)
24 opelxpi 4867 . . . . . . . . . . . . . 14  |-  ( ( s  e.  ( 0 [,] 1 )  /\  0  e.  ( 0 [,] 1 ) )  ->  <. s ,  0
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
2523, 24mpan2 666 . . . . . . . . . . . . 13  |-  ( s  e.  ( 0 [,] 1 )  ->  <. s ,  0 >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
26 fvco3 5765 . . . . . . . . . . . . 13  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  <. s ,  0
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )  -> 
( ( F  o.  A ) `  <. s ,  0 >. )  =  ( F `  ( A `  <. s ,  0 >. )
) )
2722, 25, 26syl2an 474 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. s ,  0 >. )  =  ( F `  ( A `
 <. s ,  0
>. ) ) )
28 cvmliftphtlem.c . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F  o.  A
)  =  K )
2928adantr 462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F  o.  A )  =  K )
3029fveq1d 5690 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. s ,  0 >. )  =  ( K `  <. s ,  0 >. )
)
3127, 30eqtr3d 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( A `  <. s ,  0
>. ) )  =  ( K `  <. s ,  0 >. )
)
32 df-ov 6093 . . . . . . . . . . . 12  |-  ( s A 0 )  =  ( A `  <. s ,  0 >. )
3332fveq2i 5691 . . . . . . . . . . 11  |-  ( F `
 ( s A 0 ) )  =  ( F `  ( A `  <. s ,  0 >. ) )
34 df-ov 6093 . . . . . . . . . . 11  |-  ( s K 0 )  =  ( K `  <. s ,  0 >. )
3531, 33, 343eqtr4g 2498 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( s A 0 ) )  =  ( s K 0 ) )
36 iitopon 20355 . . . . . . . . . . . . 13  |-  II  e.  (TopOn `  ( 0 [,] 1 ) )
3736a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  II  e.  (TopOn `  ( 0 [,] 1
) ) )
384, 10phtpyhtpy 20454 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G ( PHtpy `  J ) H ) 
C_  ( G ( II Htpy  J ) H ) )
3938, 11sseldd 3354 . . . . . . . . . . . 12  |-  ( ph  ->  K  e.  ( G ( II Htpy  J ) H ) )
4037, 4, 10, 39htpyi 20446 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( s K 0 )  =  ( G `
 s )  /\  ( s K 1 )  =  ( H `
 s ) ) )
4140simpld 456 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s K 0 )  =  ( G `  s ) )
4235, 41eqtrd 2473 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( s A 0 ) )  =  ( G `  s ) )
4342mpteq2dva 4375 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
s A 0 ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( G `  s ) ) )
44 fovrn 6232 . . . . . . . . . . 11  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 )  /\  0  e.  ( 0 [,] 1 ) )  ->  ( s A 0 )  e.  B )
4523, 44mp3an3 1298 . . . . . . . . . 10  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 ) )  ->  ( s A 0 )  e.  B )
4622, 45sylan 468 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s A 0 )  e.  B )
47 eqidd 2442 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )
48 cvmcn 27065 . . . . . . . . . . . 12  |-  ( F  e.  ( C CovMap  J
)  ->  F  e.  ( C  Cn  J
) )
493, 48syl 16 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( C  Cn  J ) )
50 eqid 2441 . . . . . . . . . . . 12  |-  U. J  =  U. J
511, 50cnf 18750 . . . . . . . . . . 11  |-  ( F  e.  ( C  Cn  J )  ->  F : B --> U. J )
5249, 51syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : B --> U. J
)
5352feqmptd 5741 . . . . . . . . 9  |-  ( ph  ->  F  =  ( x  e.  B  |->  ( F `
 x ) ) )
54 fveq2 5688 . . . . . . . . 9  |-  ( x  =  ( s A 0 )  ->  ( F `  x )  =  ( F `  ( s A 0 ) ) )
5546, 47, 53, 54fmptco 5873 . . . . . . . 8  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( s A 0 ) ) ) )
5619, 50cnf 18750 . . . . . . . . . 10  |-  ( G  e.  ( II  Cn  J )  ->  G : ( 0 [,] 1 ) --> U. J
)
574, 56syl 16 . . . . . . . . 9  |-  ( ph  ->  G : ( 0 [,] 1 ) --> U. J )
5857feqmptd 5741 . . . . . . . 8  |-  ( ph  ->  G  =  ( s  e.  ( 0 [,] 1 )  |->  ( G `
 s ) ) )
5943, 55, 583eqtr4d 2483 . . . . . . 7  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )  =  G )
60 cvmliftphtlem.0 . . . . . . 7  |-  ( ph  ->  ( 0 A 0 )  =  P )
6137cnmptid 19134 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  s )  e.  ( II  Cn  II ) )
6223a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ( 0 [,] 1 ) )
6337, 37, 62cnmptc 19135 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  0 )  e.  ( II  Cn  II ) )
6437, 61, 63, 17cnmpt12f 19139 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) )  e.  ( II  Cn  C ) )
651cvmlift 27102 . . . . . . . . 9  |-  ( ( ( F  e.  ( C CovMap  J )  /\  G  e.  ( II  Cn  J ) )  /\  ( P  e.  B  /\  ( F `  P
)  =  ( G `
 0 ) ) )  ->  E! f  e.  ( II  Cn  C
) ( ( F  o.  f )  =  G  /\  ( f `
 0 )  =  P ) )
663, 4, 5, 6, 65syl22anc 1214 . . . . . . . 8  |-  ( ph  ->  E! f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f ` 
0 )  =  P ) )
67 coeq2 4994 . . . . . . . . . . 11  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( F  o.  f
)  =  ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) ) ) )
6867eqeq1d 2449 . . . . . . . . . 10  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( ( F  o.  f )  =  G  <-> 
( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )  =  G ) )
69 fveq1 5687 . . . . . . . . . . . 12  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( f `  0
)  =  ( ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) `  0 ) )
70 oveq1 6097 . . . . . . . . . . . . . 14  |-  ( s  =  0  ->  (
s A 0 )  =  ( 0 A 0 ) )
71 eqid 2441 . . . . . . . . . . . . . 14  |-  ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) )  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )
72 ovex 6115 . . . . . . . . . . . . . 14  |-  ( 0 A 0 )  e. 
_V
7370, 71, 72fvmpt 5771 . . . . . . . . . . . . 13  |-  ( 0  e.  ( 0 [,] 1 )  ->  (
( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) ) `  0
)  =  ( 0 A 0 ) )
7423, 73ax-mp 5 . . . . . . . . . . . 12  |-  ( ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) `  0 )  =  ( 0 A 0 )
7569, 74syl6eq 2489 . . . . . . . . . . 11  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( f `  0
)  =  ( 0 A 0 ) )
7675eqeq1d 2449 . . . . . . . . . 10  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( ( f ` 
0 )  =  P  <-> 
( 0 A 0 )  =  P ) )
7768, 76anbi12d 705 . . . . . . . . 9  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( ( ( F  o.  f )  =  G  /\  ( f `
 0 )  =  P )  <->  ( ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) ) )  =  G  /\  (
0 A 0 )  =  P ) ) )
7877riota2 6073 . . . . . . . 8  |-  ( ( ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) )  e.  ( II  Cn  C )  /\  E! f  e.  ( II  Cn  C
) ( ( F  o.  f )  =  G  /\  ( f `
 0 )  =  P ) )  -> 
( ( ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) ) )  =  G  /\  (
0 A 0 )  =  P )  <->  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  (
f `  0 )  =  P ) )  =  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) ) ) )
7964, 66, 78syl2anc 656 . . . . . . 7  |-  ( ph  ->  ( ( ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) ) )  =  G  /\  (
0 A 0 )  =  P )  <->  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  (
f `  0 )  =  P ) )  =  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) ) ) )
8059, 60, 79mpbi2and 907 . . . . . 6  |-  ( ph  ->  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f ` 
0 )  =  P ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )
812, 80syl5eq 2485 . . . . 5  |-  ( ph  ->  M  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )
8219, 1cnf 18750 . . . . . . 7  |-  ( M  e.  ( II  Cn  C )  ->  M : ( 0 [,] 1 ) --> B )
838, 82syl 16 . . . . . 6  |-  ( ph  ->  M : ( 0 [,] 1 ) --> B )
8483feqmptd 5741 . . . . 5  |-  ( ph  ->  M  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `
 s ) ) )
8581, 84eqtr3d 2475 . . . 4  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `  s ) ) )
86 mpteqb 5785 . . . . 5  |-  ( A. s  e.  ( 0 [,] 1 ) ( s A 0 )  e.  _V  ->  (
( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `  s ) )  <->  A. s  e.  ( 0 [,] 1 ) ( s A 0 )  =  ( M `
 s ) ) )
87 ovex 6115 . . . . . 6  |-  ( s A 0 )  e. 
_V
8887a1i 11 . . . . 5  |-  ( s  e.  ( 0 [,] 1 )  ->  (
s A 0 )  e.  _V )
8986, 88mprg 2783 . . . 4  |-  ( ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `
 s ) )  <->  A. s  e.  (
0 [,] 1 ) ( s A 0 )  =  ( M `
 s ) )
9085, 89sylib 196 . . 3  |-  ( ph  ->  A. s  e.  ( 0 [,] 1 ) ( s A 0 )  =  ( M `
 s ) )
9190r19.21bi 2812 . 2  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s A 0 )  =  ( M `  s ) )
92 1elunit 11400 . . . . . . . . . . . . . 14  |-  1  e.  ( 0 [,] 1
)
93 opelxpi 4867 . . . . . . . . . . . . . 14  |-  ( ( s  e.  ( 0 [,] 1 )  /\  1  e.  ( 0 [,] 1 ) )  ->  <. s ,  1
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
9492, 93mpan2 666 . . . . . . . . . . . . 13  |-  ( s  e.  ( 0 [,] 1 )  ->  <. s ,  1 >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
95 fvco3 5765 . . . . . . . . . . . . 13  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  <. s ,  1
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )  -> 
( ( F  o.  A ) `  <. s ,  1 >. )  =  ( F `  ( A `  <. s ,  1 >. )
) )
9622, 94, 95syl2an 474 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. s ,  1 >. )  =  ( F `  ( A `
 <. s ,  1
>. ) ) )
9729fveq1d 5690 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. s ,  1 >. )  =  ( K `  <. s ,  1 >. )
)
9896, 97eqtr3d 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( A `  <. s ,  1
>. ) )  =  ( K `  <. s ,  1 >. )
)
99 df-ov 6093 . . . . . . . . . . . 12  |-  ( s A 1 )  =  ( A `  <. s ,  1 >. )
10099fveq2i 5691 . . . . . . . . . . 11  |-  ( F `
 ( s A 1 ) )  =  ( F `  ( A `  <. s ,  1 >. ) )
101 df-ov 6093 . . . . . . . . . . 11  |-  ( s K 1 )  =  ( K `  <. s ,  1 >. )
10298, 100, 1013eqtr4g 2498 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( s A 1 ) )  =  ( s K 1 ) )
10340simprd 460 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s K 1 )  =  ( H `  s ) )
104102, 103eqtrd 2473 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( s A 1 ) )  =  ( H `  s ) )
105104mpteq2dva 4375 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
s A 1 ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( H `  s ) ) )
106 fovrn 6232 . . . . . . . . . . 11  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 )  /\  1  e.  ( 0 [,] 1 ) )  ->  ( s A 1 )  e.  B )
10792, 106mp3an3 1298 . . . . . . . . . 10  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 ) )  ->  ( s A 1 )  e.  B )
10822, 107sylan 468 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s A 1 )  e.  B )
109 eqidd 2442 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )
110 fveq2 5688 . . . . . . . . 9  |-  ( x  =  ( s A 1 )  ->  ( F `  x )  =  ( F `  ( s A 1 ) ) )
111108, 109, 53, 110fmptco 5873 . . . . . . . 8  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( s A 1 ) ) ) )
11219, 50cnf 18750 . . . . . . . . . 10  |-  ( H  e.  ( II  Cn  J )  ->  H : ( 0 [,] 1 ) --> U. J
)
11310, 112syl 16 . . . . . . . . 9  |-  ( ph  ->  H : ( 0 [,] 1 ) --> U. J )
114113feqmptd 5741 . . . . . . . 8  |-  ( ph  ->  H  =  ( s  e.  ( 0 [,] 1 )  |->  ( H `
 s ) ) )
115105, 111, 1143eqtr4d 2483 . . . . . . 7  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )  =  H )
116 iicon 20363 . . . . . . . . . . . . 13  |-  II  e.  Con
117116a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  II  e.  Con )
118 iinllycon 27057 . . . . . . . . . . . . 13  |-  II  e. 𝑛Locally  Con
119118a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  II  e. 𝑛Locally  Con )
12037, 63, 61, 17cnmpt12f 19139 . . . . . . . . . . . 12  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) )  e.  ( II  Cn  C ) )
121 cvmtop1 27063 . . . . . . . . . . . . . . 15  |-  ( F  e.  ( C CovMap  J
)  ->  C  e.  Top )
1223, 121syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  Top )
1231toptopon 18438 . . . . . . . . . . . . . 14  |-  ( C  e.  Top  <->  C  e.  (TopOn `  B ) )
124122, 123sylib 196 . . . . . . . . . . . . 13  |-  ( ph  ->  C  e.  (TopOn `  B ) )
125 ffvelrn 5838 . . . . . . . . . . . . . 14  |-  ( ( M : ( 0 [,] 1 ) --> B  /\  0  e.  ( 0 [,] 1 ) )  ->  ( M `  0 )  e.  B )
12683, 23, 125sylancl 657 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M `  0
)  e.  B )
127 cnconst2 18787 . . . . . . . . . . . . 13  |-  ( ( II  e.  (TopOn `  ( 0 [,] 1
) )  /\  C  e.  (TopOn `  B )  /\  ( M `  0
)  e.  B )  ->  ( ( 0 [,] 1 )  X. 
{ ( M ` 
0 ) } )  e.  ( II  Cn  C ) )
12837, 124, 126, 127syl3anc 1213 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0 [,] 1 )  X.  {
( M `  0
) } )  e.  ( II  Cn  C
) )
1294, 10, 11phtpyi 20456 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( 0 K s )  =  ( G `
 0 )  /\  ( 1 K s )  =  ( G `
 1 ) ) )
130129simpld 456 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
0 K s )  =  ( G ` 
0 ) )
131 opelxpi 4867 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  ->  <. 0 ,  s
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
13223, 131mpan 665 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( 0 [,] 1 )  ->  <. 0 ,  s >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
133 fvco3 5765 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  <. 0 ,  s
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )  -> 
( ( F  o.  A ) `  <. 0 ,  s >. )  =  ( F `  ( A `  <. 0 ,  s >. )
) )
13422, 132, 133syl2an 474 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. 0 ,  s >. )  =  ( F `  ( A `
 <. 0 ,  s
>. ) ) )
13529fveq1d 5690 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. 0 ,  s >. )  =  ( K `  <. 0 ,  s >. )
)
136134, 135eqtr3d 2475 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( A `  <. 0 ,  s
>. ) )  =  ( K `  <. 0 ,  s >. )
)
137 df-ov 6093 . . . . . . . . . . . . . . . . . 18  |-  ( 0 A s )  =  ( A `  <. 0 ,  s >. )
138137fveq2i 5691 . . . . . . . . . . . . . . . . 17  |-  ( F `
 ( 0 A s ) )  =  ( F `  ( A `  <. 0 ,  s >. ) )
139 df-ov 6093 . . . . . . . . . . . . . . . . 17  |-  ( 0 K s )  =  ( K `  <. 0 ,  s >. )
140136, 138, 1393eqtr4g 2498 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( 0 A s ) )  =  ( 0 K s ) )
1417simp3d 997 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M `  0
)  =  P )
142141adantr 462 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( M `  0 )  =  P )
143142fveq2d 5692 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( M `  0 ) )  =  ( F `  P ) )
1446adantr 462 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  P )  =  ( G ` 
0 ) )
145143, 144eqtrd 2473 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( M `  0 ) )  =  ( G ` 
0 ) )
146130, 140, 1453eqtr4d 2483 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( 0 A s ) )  =  ( F `  ( M `  0 ) ) )
147146mpteq2dva 4375 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
0 A s ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( M `
 0 ) ) ) )
148 fconstmpt 4878 . . . . . . . . . . . . . 14  |-  ( ( 0 [,] 1 )  X.  { ( F `
 ( M ` 
0 ) ) } )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `
 ( M ` 
0 ) ) )
149147, 148syl6eqr 2491 . . . . . . . . . . . . 13  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
0 A s ) ) )  =  ( ( 0 [,] 1
)  X.  { ( F `  ( M `
 0 ) ) } ) )
150 fovrn 6232 . . . . . . . . . . . . . . . 16  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  0  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  ->  ( 0 A s )  e.  B )
15123, 150mp3an2 1297 . . . . . . . . . . . . . . 15  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 ) )  ->  ( 0 A s )  e.  B )
15222, 151sylan 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
0 A s )  e.  B )
153 eqidd 2442 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) ) )
154 fveq2 5688 . . . . . . . . . . . . . 14  |-  ( x  =  ( 0 A s )  ->  ( F `  x )  =  ( F `  ( 0 A s ) ) )
155152, 153, 53, 154fmptco 5873 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( 0 A s ) ) ) )
156 ffn 5556 . . . . . . . . . . . . . . 15  |-  ( F : B --> U. J  ->  F  Fn  B )
15752, 156syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  Fn  B )
158 fcoconst 5877 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  B  /\  ( M `  0 )  e.  B )  -> 
( F  o.  (
( 0 [,] 1
)  X.  { ( M `  0 ) } ) )  =  ( ( 0 [,] 1 )  X.  {
( F `  ( M `  0 )
) } ) )
159157, 126, 158syl2anc 656 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  o.  (
( 0 [,] 1
)  X.  { ( M `  0 ) } ) )  =  ( ( 0 [,] 1 )  X.  {
( F `  ( M `  0 )
) } ) )
160149, 155, 1593eqtr4d 2483 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) ) )  =  ( F  o.  ( ( 0 [,] 1 )  X.  { ( M `
 0 ) } ) ) )
16160, 141eqtr4d 2476 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0 A 0 )  =  ( M `
 0 ) )
162 oveq2 6098 . . . . . . . . . . . . . . 15  |-  ( s  =  0  ->  (
0 A s )  =  ( 0 A 0 ) )
163 eqid 2441 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) )  =  ( s  e.  ( 0 [,] 1
)  |->  ( 0 A s ) )
164162, 163, 72fvmpt 5771 . . . . . . . . . . . . . 14  |-  ( 0  e.  ( 0 [,] 1 )  ->  (
( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) ) `  0
)  =  ( 0 A 0 ) )
16523, 164ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) ) `  0 )  =  ( 0 A 0 )
166 fvex 5698 . . . . . . . . . . . . . . 15  |-  ( M `
 0 )  e. 
_V
167166fvconst2 5930 . . . . . . . . . . . . . 14  |-  ( 0  e.  ( 0 [,] 1 )  ->  (
( ( 0 [,] 1 )  X.  {
( M `  0
) } ) ` 
0 )  =  ( M `  0 ) )
16823, 167ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( ( 0 [,] 1
)  X.  { ( M `  0 ) } ) `  0
)  =  ( M `
 0 )
169161, 165, 1683eqtr4g 2498 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( s  e.  ( 0 [,] 1
)  |->  ( 0 A s ) ) ` 
0 )  =  ( ( ( 0 [,] 1 )  X.  {
( M `  0
) } ) ` 
0 ) )
1701, 19, 3, 117, 119, 62, 120, 128, 160, 169cvmliftmoi 27086 . . . . . . . . . . 11  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) )  =  ( ( 0 [,] 1
)  X.  { ( M `  0 ) } ) )
171 fconstmpt 4878 . . . . . . . . . . 11  |-  ( ( 0 [,] 1 )  X.  { ( M `
 0 ) } )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `
 0 ) )
172170, 171syl6eq 2489 . . . . . . . . . 10  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `  0 ) ) )
173 mpteqb 5785 . . . . . . . . . . 11  |-  ( A. s  e.  ( 0 [,] 1 ) ( 0 A s )  e.  _V  ->  (
( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `  0 ) )  <->  A. s  e.  ( 0 [,] 1 ) ( 0 A s )  =  ( M `
 0 ) ) )
174 ovex 6115 . . . . . . . . . . . 12  |-  ( 0 A s )  e. 
_V
175174a1i 11 . . . . . . . . . . 11  |-  ( s  e.  ( 0 [,] 1 )  ->  (
0 A s )  e.  _V )
176173, 175mprg 2783 . . . . . . . . . 10  |-  ( ( s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `
 0 ) )  <->  A. s  e.  (
0 [,] 1 ) ( 0 A s )  =  ( M `
 0 ) )
177172, 176sylib 196 . . . . . . . . 9  |-  ( ph  ->  A. s  e.  ( 0 [,] 1 ) ( 0 A s )  =  ( M `
 0 ) )
178 oveq2 6098 . . . . . . . . . . 11  |-  ( s  =  1  ->  (
0 A s )  =  ( 0 A 1 ) )
179178eqeq1d 2449 . . . . . . . . . 10  |-  ( s  =  1  ->  (
( 0 A s )  =  ( M `
 0 )  <->  ( 0 A 1 )  =  ( M `  0
) ) )
180179rspcv 3066 . . . . . . . . 9  |-  ( 1  e.  ( 0 [,] 1 )  ->  ( A. s  e.  (
0 [,] 1 ) ( 0 A s )  =  ( M `
 0 )  -> 
( 0 A 1 )  =  ( M `
 0 ) ) )
18192, 177, 180mpsyl 63 . . . . . . . 8  |-  ( ph  ->  ( 0 A 1 )  =  ( M `
 0 ) )
182181, 141eqtrd 2473 . . . . . . 7  |-  ( ph  ->  ( 0 A 1 )  =  P )
18392a1i 11 . . . . . . . . . 10  |-  ( ph  ->  1  e.  ( 0 [,] 1 ) )
18437, 37, 183cnmptc 19135 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  1 )  e.  ( II  Cn  II ) )
18537, 61, 184, 17cnmpt12f 19139 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) )  e.  ( II  Cn  C ) )
1861cvmlift 27102 . . . . . . . . 9  |-  ( ( ( F  e.  ( C CovMap  J )  /\  H  e.  ( II  Cn  J ) )  /\  ( P  e.  B  /\  ( F `  P
)  =  ( H `
 0 ) ) )  ->  E! f  e.  ( II  Cn  C
) ( ( F  o.  f )  =  H  /\  ( f `
 0 )  =  P ) )
1873, 10, 5, 14, 186syl22anc 1214 . . . . . . . 8  |-  ( ph  ->  E! f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  H  /\  ( f ` 
0 )  =  P ) )
188 coeq2 4994 . . . . . . . . . . 11  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( F  o.  f
)  =  ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) ) ) )
189188eqeq1d 2449 . . . . . . . . . 10  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( ( F  o.  f )  =  H  <-> 
( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )  =  H ) )
190 fveq1 5687 . . . . . . . . . . . 12  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( f `  0
)  =  ( ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) `  0 ) )
191 oveq1 6097 . . . . . . . . . . . . . 14  |-  ( s  =  0  ->  (
s A 1 )  =  ( 0 A 1 ) )
192 eqid 2441 . . . . . . . . . . . . . 14  |-  ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) )  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )
193 ovex 6115 . . . . . . . . . . . . . 14  |-  ( 0 A 1 )  e. 
_V
194191, 192, 193fvmpt 5771 . . . . . . . . . . . . 13  |-  ( 0  e.  ( 0 [,] 1 )  ->  (
( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) ) `  0
)  =  ( 0 A 1 ) )
19523, 194ax-mp 5 . . . . . . . . . . . 12  |-  ( ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) `  0 )  =  ( 0 A 1 )
196190, 195syl6eq 2489 . . . . . . . . . . 11  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( f `  0
)  =  ( 0 A 1 ) )
197196eqeq1d 2449 . . . . . . . . . 10  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( ( f ` 
0 )  =  P  <-> 
( 0 A 1 )  =  P ) )
198189, 197anbi12d 705 . . . . . . . . 9  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( ( ( F  o.  f )  =  H  /\  ( f `
 0 )  =  P )  <->  ( ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) ) )  =  H  /\  (
0 A 1 )  =  P ) ) )
199198riota2 6073 . . . . . . . 8  |-  ( ( ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) )  e.  ( II  Cn  C )  /\  E! f  e.  ( II  Cn  C
) ( ( F  o.  f )  =  H  /\  ( f `
 0 )  =  P ) )  -> 
( ( ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) ) )  =  H  /\  (
0 A 1 )  =  P )  <->  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  H  /\  (
f `  0 )  =  P ) )  =  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) ) ) )
200185, 187, 199syl2anc 656 . . . . . . 7  |-  ( ph  ->  ( ( ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) ) )  =  H  /\  (
0 A 1 )  =  P )  <->  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  H  /\  (
f `  0 )  =  P ) )  =  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) ) ) )
201115, 182, 200mpbi2and 907 . . . . . 6  |-  ( ph  ->  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  H  /\  ( f ` 
0 )  =  P ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )
2029, 201syl5eq 2485 . . . . 5  |-  ( ph  ->  N  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )
20319, 1cnf 18750 . . . . . . 7  |-  ( N  e.  ( II  Cn  C )  ->  N : ( 0 [,] 1 ) --> B )
20416, 203syl 16 . . . . . 6  |-  ( ph  ->  N : ( 0 [,] 1 ) --> B )
205204feqmptd 5741 . . . . 5  |-  ( ph  ->  N  =  ( s  e.  ( 0 [,] 1 )  |->  ( N `
 s ) ) )
206202, 205eqtr3d 2475 . . . 4  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( N `  s ) ) )
207 mpteqb 5785 . . . . 5  |-  ( A. s  e.  ( 0 [,] 1 ) ( s A 1 )  e.  _V  ->  (
( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( N `  s ) )  <->  A. s  e.  ( 0 [,] 1 ) ( s A 1 )  =  ( N `
 s ) ) )
208 ovex 6115 . . . . . 6  |-  ( s A 1 )  e. 
_V
209208a1i 11 . . . . 5  |-  ( s  e.  ( 0 [,] 1 )  ->  (
s A 1 )  e.  _V )
210207, 209mprg 2783 . . . 4  |-  ( ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( N `
 s ) )  <->  A. s  e.  (
0 [,] 1 ) ( s A 1 )  =  ( N `
 s ) )
211206, 210sylib 196 . . 3  |-  ( ph  ->  A. s  e.  ( 0 [,] 1 ) ( s A 1 )  =  ( N `
 s ) )
212211r19.21bi 2812 . 2  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s A 1 )  =  ( N `  s ) )
213177r19.21bi 2812 . 2  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
0 A s )  =  ( M ` 
0 ) )
21437, 184, 61, 17cnmpt12f 19139 . . . . . 6  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) )  e.  ( II  Cn  C ) )
215 ffvelrn 5838 . . . . . . . 8  |-  ( ( M : ( 0 [,] 1 ) --> B  /\  1  e.  ( 0 [,] 1 ) )  ->  ( M `  1 )  e.  B )
21683, 92, 215sylancl 657 . . . . . . 7  |-  ( ph  ->  ( M `  1
)  e.  B )
217 cnconst2 18787 . . . . . . 7  |-  ( ( II  e.  (TopOn `  ( 0 [,] 1
) )  /\  C  e.  (TopOn `  B )  /\  ( M `  1
)  e.  B )  ->  ( ( 0 [,] 1 )  X. 
{ ( M ` 
1 ) } )  e.  ( II  Cn  C ) )
21837, 124, 216, 217syl3anc 1213 . . . . . 6  |-  ( ph  ->  ( ( 0 [,] 1 )  X.  {
( M `  1
) } )  e.  ( II  Cn  C
) )
219 opelxpi 4867 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  ->  <. 1 ,  s
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
22092, 219mpan 665 . . . . . . . . . . . . 13  |-  ( s  e.  ( 0 [,] 1 )  ->  <. 1 ,  s >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
221 fvco3 5765 . . . . . . . . . . . . 13  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  <. 1 ,  s
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )  -> 
( ( F  o.  A ) `  <. 1 ,  s >. )  =  ( F `  ( A `  <. 1 ,  s >. )
) )
22222, 220, 221syl2an 474 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. 1 ,  s >. )  =  ( F `  ( A `
 <. 1 ,  s
>. ) ) )
22329fveq1d 5690 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. 1 ,  s >. )  =  ( K `  <. 1 ,  s >. )
)
224222, 223eqtr3d 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( A `  <. 1 ,  s
>. ) )  =  ( K `  <. 1 ,  s >. )
)
225 df-ov 6093 . . . . . . . . . . . 12  |-  ( 1 A s )  =  ( A `  <. 1 ,  s >. )
226225fveq2i 5691 . . . . . . . . . . 11  |-  ( F `
 ( 1 A s ) )  =  ( F `  ( A `  <. 1 ,  s >. ) )
227 df-ov 6093 . . . . . . . . . . 11  |-  ( 1 K s )  =  ( K `  <. 1 ,  s >. )
228224, 226, 2273eqtr4g 2498 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( 1 A s ) )  =  ( 1 K s ) )
229129simprd 460 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
1 K s )  =  ( G ` 
1 ) )
2307simp2d 996 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  o.  M
)  =  G )
231230adantr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F  o.  M )  =  G )
232231fveq1d 5690 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  M
) `  1 )  =  ( G ` 
1 ) )
23383adantr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  M : ( 0 [,] 1 ) --> B )
234 fvco3 5765 . . . . . . . . . . . 12  |-  ( ( M : ( 0 [,] 1 ) --> B  /\  1  e.  ( 0 [,] 1 ) )  ->  ( ( F  o.  M ) `  1 )  =  ( F `  ( M `  1 )
) )
235233, 92, 234sylancl 657 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  M
) `  1 )  =  ( F `  ( M `  1 ) ) )
236232, 235eqtr3d 2475 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( G `  1 )  =  ( F `  ( M `  1 ) ) )
237228, 229, 2363eqtrd 2477 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( 1 A s ) )  =  ( F `  ( M `  1 ) ) )
238237mpteq2dva 4375 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
1 A s ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( M `
 1 ) ) ) )
239 fconstmpt 4878 . . . . . . . 8  |-  ( ( 0 [,] 1 )  X.  { ( F `
 ( M ` 
1 ) ) } )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `
 ( M ` 
1 ) ) )
240238, 239syl6eqr 2491 . . . . . . 7  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
1 A s ) ) )  =  ( ( 0 [,] 1
)  X.  { ( F `  ( M `
 1 ) ) } ) )
241 fovrn 6232 . . . . . . . . . 10  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  1  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  ->  ( 1 A s )  e.  B )
24292, 241mp3an2 1297 . . . . . . . . 9  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 ) )  ->  ( 1 A s )  e.  B )
24322, 242sylan 468 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
1 A s )  e.  B )
244 eqidd 2442 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) ) )
245 fveq2 5688 . . . . . . . 8  |-  ( x  =  ( 1 A s )  ->  ( F `  x )  =  ( F `  ( 1 A s ) ) )
246243, 244, 53, 245fmptco 5873 . . . . . . 7  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( 1 A s ) ) ) )
247 fcoconst 5877 . . . . . . . 8  |-  ( ( F  Fn  B  /\  ( M `  1 )  e.  B )  -> 
( F  o.  (
( 0 [,] 1
)  X.  { ( M `  1 ) } ) )  =  ( ( 0 [,] 1 )  X.  {
( F `  ( M `  1 )
) } ) )
248157, 216, 247syl2anc 656 . . . . . . 7  |-  ( ph  ->  ( F  o.  (
( 0 [,] 1
)  X.  { ( M `  1 ) } ) )  =  ( ( 0 [,] 1 )  X.  {
( F `  ( M `  1 )
) } ) )
249240, 246, 2483eqtr4d 2483 . . . . . 6  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) ) )  =  ( F  o.  ( ( 0 [,] 1 )  X.  { ( M `
 1 ) } ) ) )
250 oveq1 6097 . . . . . . . . . 10  |-  ( s  =  1  ->  (
s A 0 )  =  ( 1 A 0 ) )
251 fveq2 5688 . . . . . . . . . 10  |-  ( s  =  1  ->  ( M `  s )  =  ( M ` 
1 ) )
252250, 251eqeq12d 2455 . . . . . . . . 9  |-  ( s  =  1  ->  (
( s A 0 )  =  ( M `
 s )  <->  ( 1 A 0 )  =  ( M `  1
) ) )
253252rspcv 3066 . . . . . . . 8  |-  ( 1  e.  ( 0 [,] 1 )  ->  ( A. s  e.  (
0 [,] 1 ) ( s A 0 )  =  ( M `
 s )  -> 
( 1 A 0 )  =  ( M `
 1 ) ) )
25492, 90, 253mpsyl 63 . . . . . . 7  |-  ( ph  ->  ( 1 A 0 )  =  ( M `
 1 ) )
255 oveq2 6098 . . . . . . . . 9  |-  ( s  =  0  ->  (
1 A s )  =  ( 1 A 0 ) )
256 eqid 2441 . . . . . . . . 9  |-  ( s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) )  =  ( s  e.  ( 0 [,] 1
)  |->  ( 1 A s ) )
257 ovex 6115 . . . . . . . . 9  |-  ( 1 A 0 )  e. 
_V
258255, 256, 257fvmpt 5771 . . . . . . . 8  |-  ( 0  e.  ( 0 [,] 1 )  ->  (
( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) ) `  0
)  =  ( 1 A 0 ) )
25923, 258ax-mp 5 . . . . . . 7  |-  ( ( s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) ) `  0 )  =  ( 1 A 0 )
260 fvex 5698 . . . . . . . . 9  |-  ( M `
 1 )  e. 
_V
261260fvconst2 5930 . . . . . . . 8  |-  ( 0  e.  ( 0 [,] 1 )  ->  (
( ( 0 [,] 1 )  X.  {
( M `  1
) } ) ` 
0 )  =  ( M `  1 ) )
26223, 261ax-mp 5 . . . . . . 7  |-  ( ( ( 0 [,] 1
)  X.  { ( M `  1 ) } ) `  0
)  =  ( M `
 1 )
263254, 259, 2623eqtr4g 2498 . . . . . 6  |-  ( ph  ->  ( ( s  e.  ( 0 [,] 1
)  |->  ( 1 A s ) ) ` 
0 )  =  ( ( ( 0 [,] 1 )  X.  {
( M `  1
) } ) ` 
0 ) )
2641, 19, 3, 117, 119, 62, 214, 218, 249, 263cvmliftmoi 27086 . . . . 5  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) )  =  ( ( 0 [,] 1
)  X.  { ( M `  1 ) } ) )
265 fconstmpt 4878 . . . . 5  |-  ( ( 0 [,] 1 )  X.  { ( M `
 1 ) } )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `
 1 ) )
266264, 265syl6eq 2489 . . . 4  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `  1 ) ) )
267 mpteqb 5785 . . . . 5  |-  ( A. s  e.  ( 0 [,] 1 ) ( 1 A s )  e.  _V  ->  (
( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `  1 ) )  <->  A. s  e.  ( 0 [,] 1 ) ( 1 A s )  =  ( M `
 1 ) ) )
268 ovex 6115 . . . . . 6  |-  ( 1 A s )  e. 
_V
269268a1i 11 . . . . 5  |-  ( s  e.  ( 0 [,] 1 )  ->  (
1 A s )  e.  _V )
270267, 269mprg 2783 . . . 4  |-  ( ( s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `
 1 ) )  <->  A. s  e.  (
0 [,] 1 ) ( 1 A s )  =  ( M `
 1 ) )
271266, 270sylib 196 . . 3  |-  ( ph  ->  A. s  e.  ( 0 [,] 1 ) ( 1 A s )  =  ( M `
 1 ) )
272271r19.21bi 2812 . 2  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
1 A s )  =  ( M ` 
1 ) )
2738, 16, 17, 91, 212, 213, 272isphtpy2d 20459 1  |-  ( ph  ->  A  e.  ( M ( PHtpy `  C ) N ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364    e. wcel 1761   A.wral 2713   E!wreu 2715   _Vcvv 2970   {csn 3874   <.cop 3880   U.cuni 4088    e. cmpt 4347    X. cxp 4834    o. ccom 4840    Fn wfn 5410   -->wf 5411   ` cfv 5415   iota_crio 6048  (class class class)co 6090   0cc0 9278   1c1 9279   [,]cicc 11299   Topctop 18398  TopOnctopon 18399    Cn ccn 18728   Conccon 18915  𝑛Locally cnlly 18969    tX ctx 19033   IIcii 20351   Htpy chtpy 20439   PHtpycphtpy 20440   CovMap ccvm 27058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355  ax-pre-sup 9356  ax-addf 9357  ax-mulf 9358
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-iin 4171  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-of 6319  df-om 6476  df-1st 6576  df-2nd 6577  df-supp 6690  df-recs 6828  df-rdg 6862  df-1o 6916  df-2o 6917  df-oadd 6920  df-er 7097  df-ec 7099  df-map 7212  df-ixp 7260  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-fsupp 7617  df-fi 7657  df-sup 7687  df-oi 7720  df-card 8105  df-cda 8333  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-div 9990  df-nn 10319  df-2 10376  df-3 10377  df-4 10378  df-5 10379  df-6 10380  df-7 10381  df-8 10382  df-9 10383  df-10 10384  df-n0 10576  df-z 10643  df-dec 10752  df-uz 10858  df-q 10950  df-rp 10988  df-xneg 11085  df-xadd 11086  df-xmul 11087  df-ioo 11300  df-ico 11302  df-icc 11303  df-fz 11434  df-fzo 11545  df-fl 11638  df-seq 11803  df-exp 11862  df-hash 12100  df-cj 12584  df-re 12585  df-im 12586  df-sqr 12720  df-abs 12721  df-clim 12962  df-sum 13160  df-struct 14172  df-ndx 14173  df-slot 14174  df-base 14175  df-sets 14176  df-ress 14177  df-plusg 14247  df-mulr 14248  df-starv 14249  df-sca 14250  df-vsca 14251  df-ip 14252  df-tset 14253  df-ple 14254  df-ds 14256  df-unif 14257  df-hom 14258  df-cco 14259  df-rest 14357  df-topn 14358  df-0g 14376  df-gsum 14377  df-topgen 14378  df-pt 14379  df-prds 14382  df-xrs 14436  df-qtop 14441  df-imas 14442  df-xps 14444  df-mre 14520  df-mrc 14521  df-acs 14523  df-mnd 15411  df-submnd 15461  df-mulg 15541  df-cntz 15828  df-cmn 16272  df-psmet 17709  df-xmet 17710  df-met 17711  df-bl 17712  df-mopn 17713  df-cnfld 17719  df-top 18403  df-bases 18405  df-topon 18406  df-topsp 18407  df-cld 18523  df-ntr 18524  df-cls 18525  df-nei 18602  df-cn 18731  df-cnp 18732  df-cmp 18890  df-con 18916  df-lly 18970  df-nlly 18971  df-tx 19035  df-hmeo 19228  df-xms 19795  df-ms 19796  df-tms 19797  df-ii 20353  df-htpy 20442  df-phtpy 20443  df-phtpc 20464  df-pcon 27024  df-scon 27025  df-cvm 27059
This theorem is referenced by:  cvmliftpht  27121
  Copyright terms: Public domain W3C validator