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

Theorem cvmliftphtlem 27206
Description: Lemma for cvmliftpht 27207. (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 27190 . . 3  |-  ( ph  ->  ( M  e.  ( II  Cn  C )  /\  ( F  o.  M )  =  G  /\  ( M ` 
0 )  =  P ) )
87simp1d 1000 . 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 20557 . . . . . 6  |-  ( ph  ->  ( ( G ` 
0 )  =  ( H `  0 )  /\  ( G ` 
1 )  =  ( H `  1 ) ) )
1312simpld 459 . . . . 5  |-  ( ph  ->  ( G `  0
)  =  ( H `
 0 ) )
146, 13eqtrd 2475 . . . 4  |-  ( ph  ->  ( F `  P
)  =  ( H `
 0 ) )
151, 9, 3, 10, 5, 14cvmliftiota 27190 . . 3  |-  ( ph  ->  ( N  e.  ( II  Cn  C )  /\  ( F  o.  N )  =  H  /\  ( N ` 
0 )  =  P ) )
1615simp1d 1000 . 2  |-  ( ph  ->  N  e.  ( II 
Cn  C ) )
17 cvmliftphtlem.a . 2  |-  ( ph  ->  A  e.  ( ( II  tX  II )  Cn  C ) )
18 iitop 20456 . . . . . . . . . . . . . . . 16  |-  II  e.  Top
19 iiuni 20457 . . . . . . . . . . . . . . . 16  |-  ( 0 [,] 1 )  = 
U. II
2018, 18, 19, 19txunii 19166 . . . . . . . . . . . . . . 15  |-  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )  = 
U. ( II  tX  II )
2120, 1cnf 18850 . . . . . . . . . . . . . 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 11403 . . . . . . . . . . . . . 14  |-  0  e.  ( 0 [,] 1
)
24 opelxpi 4871 . . . . . . . . . . . . . 14  |-  ( ( s  e.  ( 0 [,] 1 )  /\  0  e.  ( 0 [,] 1 ) )  ->  <. s ,  0
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
2523, 24mpan2 671 . . . . . . . . . . . . 13  |-  ( s  e.  ( 0 [,] 1 )  ->  <. s ,  0 >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
26 fvco3 5768 . . . . . . . . . . . . 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 477 . . . . . . . . . . . 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 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F  o.  A )  =  K )
3029fveq1d 5693 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. s ,  0 >. )  =  ( K `  <. s ,  0 >. )
)
3127, 30eqtr3d 2477 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( A `  <. s ,  0
>. ) )  =  ( K `  <. s ,  0 >. )
)
32 df-ov 6094 . . . . . . . . . . . 12  |-  ( s A 0 )  =  ( A `  <. s ,  0 >. )
3332fveq2i 5694 . . . . . . . . . . 11  |-  ( F `
 ( s A 0 ) )  =  ( F `  ( A `  <. s ,  0 >. ) )
34 df-ov 6094 . . . . . . . . . . 11  |-  ( s K 0 )  =  ( K `  <. s ,  0 >. )
3531, 33, 343eqtr4g 2500 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( s A 0 ) )  =  ( s K 0 ) )
36 iitopon 20455 . . . . . . . . . . . . 13  |-  II  e.  (TopOn `  ( 0 [,] 1 ) )
3736a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  II  e.  (TopOn `  ( 0 [,] 1
) ) )
384, 10phtpyhtpy 20554 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G ( PHtpy `  J ) H ) 
C_  ( G ( II Htpy  J ) H ) )
3938, 11sseldd 3357 . . . . . . . . . . . 12  |-  ( ph  ->  K  e.  ( G ( II Htpy  J ) H ) )
4037, 4, 10, 39htpyi 20546 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( s K 0 )  =  ( G `
 s )  /\  ( s K 1 )  =  ( H `
 s ) ) )
4140simpld 459 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s K 0 )  =  ( G `  s ) )
4235, 41eqtrd 2475 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( s A 0 ) )  =  ( G `  s ) )
4342mpteq2dva 4378 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
s A 0 ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( G `  s ) ) )
44 fovrn 6233 . . . . . . . . . . 11  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 )  /\  0  e.  ( 0 [,] 1 ) )  ->  ( s A 0 )  e.  B )
4523, 44mp3an3 1303 . . . . . . . . . 10  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 ) )  ->  ( s A 0 )  e.  B )
4622, 45sylan 471 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s A 0 )  e.  B )
47 eqidd 2444 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )
48 cvmcn 27151 . . . . . . . . . . . 12  |-  ( F  e.  ( C CovMap  J
)  ->  F  e.  ( C  Cn  J
) )
493, 48syl 16 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( C  Cn  J ) )
50 eqid 2443 . . . . . . . . . . . 12  |-  U. J  =  U. J
511, 50cnf 18850 . . . . . . . . . . 11  |-  ( F  e.  ( C  Cn  J )  ->  F : B --> U. J )
5249, 51syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : B --> U. J
)
5352feqmptd 5744 . . . . . . . . 9  |-  ( ph  ->  F  =  ( x  e.  B  |->  ( F `
 x ) ) )
54 fveq2 5691 . . . . . . . . 9  |-  ( x  =  ( s A 0 )  ->  ( F `  x )  =  ( F `  ( s A 0 ) ) )
5546, 47, 53, 54fmptco 5876 . . . . . . . 8  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( s A 0 ) ) ) )
5619, 50cnf 18850 . . . . . . . . . 10  |-  ( G  e.  ( II  Cn  J )  ->  G : ( 0 [,] 1 ) --> U. J
)
574, 56syl 16 . . . . . . . . 9  |-  ( ph  ->  G : ( 0 [,] 1 ) --> U. J )
5857feqmptd 5744 . . . . . . . 8  |-  ( ph  ->  G  =  ( s  e.  ( 0 [,] 1 )  |->  ( G `
 s ) ) )
5943, 55, 583eqtr4d 2485 . . . . . . 7  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )  =  G )
60 cvmliftphtlem.0 . . . . . . 7  |-  ( ph  ->  ( 0 A 0 )  =  P )
6137cnmptid 19234 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  s )  e.  ( II  Cn  II ) )
6223a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ( 0 [,] 1 ) )
6337, 37, 62cnmptc 19235 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  0 )  e.  ( II  Cn  II ) )
6437, 61, 63, 17cnmpt12f 19239 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) )  e.  ( II  Cn  C ) )
651cvmlift 27188 . . . . . . . . 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 1219 . . . . . . . 8  |-  ( ph  ->  E! f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f ` 
0 )  =  P ) )
67 coeq2 4998 . . . . . . . . . . 11  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( F  o.  f
)  =  ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) ) ) )
6867eqeq1d 2451 . . . . . . . . . 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 5690 . . . . . . . . . . . 12  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( f `  0
)  =  ( ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) `  0 ) )
70 oveq1 6098 . . . . . . . . . . . . . 14  |-  ( s  =  0  ->  (
s A 0 )  =  ( 0 A 0 ) )
71 eqid 2443 . . . . . . . . . . . . . 14  |-  ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) )  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )
72 ovex 6116 . . . . . . . . . . . . . 14  |-  ( 0 A 0 )  e. 
_V
7370, 71, 72fvmpt 5774 . . . . . . . . . . . . 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 2491 . . . . . . . . . . 11  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( f `  0
)  =  ( 0 A 0 ) )
7675eqeq1d 2451 . . . . . . . . . 10  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 0 ) )  -> 
( ( f ` 
0 )  =  P  <-> 
( 0 A 0 )  =  P ) )
7768, 76anbi12d 710 . . . . . . . . 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 6075 . . . . . . . 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 661 . . . . . . 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 912 . . . . . 6  |-  ( ph  ->  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  G  /\  ( f ` 
0 )  =  P ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )
812, 80syl5eq 2487 . . . . 5  |-  ( ph  ->  M  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 0 ) ) )
8219, 1cnf 18850 . . . . . . 7  |-  ( M  e.  ( II  Cn  C )  ->  M : ( 0 [,] 1 ) --> B )
838, 82syl 16 . . . . . 6  |-  ( ph  ->  M : ( 0 [,] 1 ) --> B )
8483feqmptd 5744 . . . . 5  |-  ( ph  ->  M  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `
 s ) ) )
8581, 84eqtr3d 2477 . . . 4  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 0 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `  s ) ) )
86 mpteqb 5788 . . . . 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 6116 . . . . . 6  |-  ( s A 0 )  e. 
_V
8887a1i 11 . . . . 5  |-  ( s  e.  ( 0 [,] 1 )  ->  (
s A 0 )  e.  _V )
8986, 88mprg 2785 . . . 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 2814 . 2  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s A 0 )  =  ( M `  s ) )
92 1elunit 11404 . . . . . . . . . . . . . 14  |-  1  e.  ( 0 [,] 1
)
93 opelxpi 4871 . . . . . . . . . . . . . 14  |-  ( ( s  e.  ( 0 [,] 1 )  /\  1  e.  ( 0 [,] 1 ) )  ->  <. s ,  1
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
9492, 93mpan2 671 . . . . . . . . . . . . 13  |-  ( s  e.  ( 0 [,] 1 )  ->  <. s ,  1 >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
95 fvco3 5768 . . . . . . . . . . . . 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 477 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. s ,  1 >. )  =  ( F `  ( A `
 <. s ,  1
>. ) ) )
9729fveq1d 5693 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. s ,  1 >. )  =  ( K `  <. s ,  1 >. )
)
9896, 97eqtr3d 2477 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( A `  <. s ,  1
>. ) )  =  ( K `  <. s ,  1 >. )
)
99 df-ov 6094 . . . . . . . . . . . 12  |-  ( s A 1 )  =  ( A `  <. s ,  1 >. )
10099fveq2i 5694 . . . . . . . . . . 11  |-  ( F `
 ( s A 1 ) )  =  ( F `  ( A `  <. s ,  1 >. ) )
101 df-ov 6094 . . . . . . . . . . 11  |-  ( s K 1 )  =  ( K `  <. s ,  1 >. )
10298, 100, 1013eqtr4g 2500 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( s A 1 ) )  =  ( s K 1 ) )
10340simprd 463 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s K 1 )  =  ( H `  s ) )
104102, 103eqtrd 2475 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( s A 1 ) )  =  ( H `  s ) )
105104mpteq2dva 4378 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
s A 1 ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( H `  s ) ) )
106 fovrn 6233 . . . . . . . . . . 11  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 )  /\  1  e.  ( 0 [,] 1 ) )  ->  ( s A 1 )  e.  B )
10792, 106mp3an3 1303 . . . . . . . . . 10  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 ) )  ->  ( s A 1 )  e.  B )
10822, 107sylan 471 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s A 1 )  e.  B )
109 eqidd 2444 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )
110 fveq2 5691 . . . . . . . . 9  |-  ( x  =  ( s A 1 )  ->  ( F `  x )  =  ( F `  ( s A 1 ) ) )
111108, 109, 53, 110fmptco 5876 . . . . . . . 8  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( s A 1 ) ) ) )
11219, 50cnf 18850 . . . . . . . . . 10  |-  ( H  e.  ( II  Cn  J )  ->  H : ( 0 [,] 1 ) --> U. J
)
11310, 112syl 16 . . . . . . . . 9  |-  ( ph  ->  H : ( 0 [,] 1 ) --> U. J )
114113feqmptd 5744 . . . . . . . 8  |-  ( ph  ->  H  =  ( s  e.  ( 0 [,] 1 )  |->  ( H `
 s ) ) )
115105, 111, 1143eqtr4d 2485 . . . . . . 7  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )  =  H )
116 iicon 20463 . . . . . . . . . . . . 13  |-  II  e.  Con
117116a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  II  e.  Con )
118 iinllycon 27143 . . . . . . . . . . . . 13  |-  II  e. 𝑛Locally  Con
119118a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  II  e. 𝑛Locally  Con )
12037, 63, 61, 17cnmpt12f 19239 . . . . . . . . . . . 12  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) )  e.  ( II  Cn  C ) )
121 cvmtop1 27149 . . . . . . . . . . . . . . 15  |-  ( F  e.  ( C CovMap  J
)  ->  C  e.  Top )
1223, 121syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  Top )
1231toptopon 18538 . . . . . . . . . . . . . 14  |-  ( C  e.  Top  <->  C  e.  (TopOn `  B ) )
124122, 123sylib 196 . . . . . . . . . . . . 13  |-  ( ph  ->  C  e.  (TopOn `  B ) )
125 ffvelrn 5841 . . . . . . . . . . . . . 14  |-  ( ( M : ( 0 [,] 1 ) --> B  /\  0  e.  ( 0 [,] 1 ) )  ->  ( M `  0 )  e.  B )
12683, 23, 125sylancl 662 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M `  0
)  e.  B )
127 cnconst2 18887 . . . . . . . . . . . . 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 1218 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0 [,] 1 )  X.  {
( M `  0
) } )  e.  ( II  Cn  C
) )
1294, 10, 11phtpyi 20556 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( 0 K s )  =  ( G `
 0 )  /\  ( 1 K s )  =  ( G `
 1 ) ) )
130129simpld 459 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
0 K s )  =  ( G ` 
0 ) )
131 opelxpi 4871 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 0  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  ->  <. 0 ,  s
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
13223, 131mpan 670 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( 0 [,] 1 )  ->  <. 0 ,  s >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
133 fvco3 5768 . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. 0 ,  s >. )  =  ( F `  ( A `
 <. 0 ,  s
>. ) ) )
13529fveq1d 5693 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. 0 ,  s >. )  =  ( K `  <. 0 ,  s >. )
)
136134, 135eqtr3d 2477 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( A `  <. 0 ,  s
>. ) )  =  ( K `  <. 0 ,  s >. )
)
137 df-ov 6094 . . . . . . . . . . . . . . . . . 18  |-  ( 0 A s )  =  ( A `  <. 0 ,  s >. )
138137fveq2i 5694 . . . . . . . . . . . . . . . . 17  |-  ( F `
 ( 0 A s ) )  =  ( F `  ( A `  <. 0 ,  s >. ) )
139 df-ov 6094 . . . . . . . . . . . . . . . . 17  |-  ( 0 K s )  =  ( K `  <. 0 ,  s >. )
140136, 138, 1393eqtr4g 2500 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( 0 A s ) )  =  ( 0 K s ) )
1417simp3d 1002 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M `  0
)  =  P )
142141adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( M `  0 )  =  P )
143142fveq2d 5695 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( M `  0 ) )  =  ( F `  P ) )
1446adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  P )  =  ( G ` 
0 ) )
145143, 144eqtrd 2475 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( M `  0 ) )  =  ( G ` 
0 ) )
146130, 140, 1453eqtr4d 2485 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( 0 A s ) )  =  ( F `  ( M `  0 ) ) )
147146mpteq2dva 4378 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
0 A s ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( M `
 0 ) ) ) )
148 fconstmpt 4882 . . . . . . . . . . . . . 14  |-  ( ( 0 [,] 1 )  X.  { ( F `
 ( M ` 
0 ) ) } )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `
 ( M ` 
0 ) ) )
149147, 148syl6eqr 2493 . . . . . . . . . . . . 13  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
0 A s ) ) )  =  ( ( 0 [,] 1
)  X.  { ( F `  ( M `
 0 ) ) } ) )
150 fovrn 6233 . . . . . . . . . . . . . . . 16  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  0  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  ->  ( 0 A s )  e.  B )
15123, 150mp3an2 1302 . . . . . . . . . . . . . . 15  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 ) )  ->  ( 0 A s )  e.  B )
15222, 151sylan 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
0 A s )  e.  B )
153 eqidd 2444 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) ) )
154 fveq2 5691 . . . . . . . . . . . . . 14  |-  ( x  =  ( 0 A s )  ->  ( F `  x )  =  ( F `  ( 0 A s ) ) )
155152, 153, 53, 154fmptco 5876 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( 0 A s ) ) ) )
156 ffn 5559 . . . . . . . . . . . . . . 15  |-  ( F : B --> U. J  ->  F  Fn  B )
15752, 156syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  Fn  B )
158 fcoconst 5880 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  B  /\  ( M `  0 )  e.  B )  -> 
( F  o.  (
( 0 [,] 1
)  X.  { ( M `  0 ) } ) )  =  ( ( 0 [,] 1 )  X.  {
( F `  ( M `  0 )
) } ) )
159157, 126, 158syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  o.  (
( 0 [,] 1
)  X.  { ( M `  0 ) } ) )  =  ( ( 0 [,] 1 )  X.  {
( F `  ( M `  0 )
) } ) )
160149, 155, 1593eqtr4d 2485 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) ) )  =  ( F  o.  ( ( 0 [,] 1 )  X.  { ( M `
 0 ) } ) ) )
16160, 141eqtr4d 2478 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0 A 0 )  =  ( M `
 0 ) )
162 oveq2 6099 . . . . . . . . . . . . . . 15  |-  ( s  =  0  ->  (
0 A s )  =  ( 0 A 0 ) )
163 eqid 2443 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( 0 [,] 1 )  |->  ( 0 A s ) )  =  ( s  e.  ( 0 [,] 1
)  |->  ( 0 A s ) )
164162, 163, 72fvmpt 5774 . . . . . . . . . . . . . 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 5701 . . . . . . . . . . . . . . 15  |-  ( M `
 0 )  e. 
_V
167166fvconst2 5933 . . . . . . . . . . . . . 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 2500 . . . . . . . . . . . 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 27172 . . . . . . . . . . 11  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) )  =  ( ( 0 [,] 1
)  X.  { ( M `  0 ) } ) )
171 fconstmpt 4882 . . . . . . . . . . 11  |-  ( ( 0 [,] 1 )  X.  { ( M `
 0 ) } )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `
 0 ) )
172170, 171syl6eq 2491 . . . . . . . . . 10  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 0 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `  0 ) ) )
173 mpteqb 5788 . . . . . . . . . . 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 6116 . . . . . . . . . . . 12  |-  ( 0 A s )  e. 
_V
175174a1i 11 . . . . . . . . . . 11  |-  ( s  e.  ( 0 [,] 1 )  ->  (
0 A s )  e.  _V )
176173, 175mprg 2785 . . . . . . . . . 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 6099 . . . . . . . . . . 11  |-  ( s  =  1  ->  (
0 A s )  =  ( 0 A 1 ) )
179178eqeq1d 2451 . . . . . . . . . 10  |-  ( s  =  1  ->  (
( 0 A s )  =  ( M `
 0 )  <->  ( 0 A 1 )  =  ( M `  0
) ) )
180179rspcv 3069 . . . . . . . . 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 2475 . . . . . . 7  |-  ( ph  ->  ( 0 A 1 )  =  P )
18392a1i 11 . . . . . . . . . 10  |-  ( ph  ->  1  e.  ( 0 [,] 1 ) )
18437, 37, 183cnmptc 19235 . . . . . . . . 9  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  1 )  e.  ( II  Cn  II ) )
18537, 61, 184, 17cnmpt12f 19239 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) )  e.  ( II  Cn  C ) )
1861cvmlift 27188 . . . . . . . . 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 1219 . . . . . . . 8  |-  ( ph  ->  E! f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  H  /\  ( f ` 
0 )  =  P ) )
188 coeq2 4998 . . . . . . . . . . 11  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( F  o.  f
)  =  ( F  o.  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) ) ) )
189188eqeq1d 2451 . . . . . . . . . 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 5690 . . . . . . . . . . . 12  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( f `  0
)  =  ( ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) `  0 ) )
191 oveq1 6098 . . . . . . . . . . . . . 14  |-  ( s  =  0  ->  (
s A 1 )  =  ( 0 A 1 ) )
192 eqid 2443 . . . . . . . . . . . . . 14  |-  ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) )  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )
193 ovex 6116 . . . . . . . . . . . . . 14  |-  ( 0 A 1 )  e. 
_V
194191, 192, 193fvmpt 5774 . . . . . . . . . . . . 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 2491 . . . . . . . . . . 11  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( f `  0
)  =  ( 0 A 1 ) )
197196eqeq1d 2451 . . . . . . . . . 10  |-  ( f  =  ( s  e.  ( 0 [,] 1
)  |->  ( s A 1 ) )  -> 
( ( f ` 
0 )  =  P  <-> 
( 0 A 1 )  =  P ) )
198189, 197anbi12d 710 . . . . . . . . 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 6075 . . . . . . . 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 661 . . . . . . 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 912 . . . . . 6  |-  ( ph  ->  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  H  /\  ( f ` 
0 )  =  P ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )
2029, 201syl5eq 2487 . . . . 5  |-  ( ph  ->  N  =  ( s  e.  ( 0 [,] 1 )  |->  ( s A 1 ) ) )
20319, 1cnf 18850 . . . . . . 7  |-  ( N  e.  ( II  Cn  C )  ->  N : ( 0 [,] 1 ) --> B )
20416, 203syl 16 . . . . . 6  |-  ( ph  ->  N : ( 0 [,] 1 ) --> B )
205204feqmptd 5744 . . . . 5  |-  ( ph  ->  N  =  ( s  e.  ( 0 [,] 1 )  |->  ( N `
 s ) ) )
206202, 205eqtr3d 2477 . . . 4  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( s A 1 ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( N `  s ) ) )
207 mpteqb 5788 . . . . 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 6116 . . . . . 6  |-  ( s A 1 )  e. 
_V
209208a1i 11 . . . . 5  |-  ( s  e.  ( 0 [,] 1 )  ->  (
s A 1 )  e.  _V )
210207, 209mprg 2785 . . . 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 2814 . 2  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
s A 1 )  =  ( N `  s ) )
213177r19.21bi 2814 . 2  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
0 A s )  =  ( M ` 
0 ) )
21437, 184, 61, 17cnmpt12f 19239 . . . . . 6  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) )  e.  ( II  Cn  C ) )
215 ffvelrn 5841 . . . . . . . 8  |-  ( ( M : ( 0 [,] 1 ) --> B  /\  1  e.  ( 0 [,] 1 ) )  ->  ( M `  1 )  e.  B )
21683, 92, 215sylancl 662 . . . . . . 7  |-  ( ph  ->  ( M `  1
)  e.  B )
217 cnconst2 18887 . . . . . . 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 1218 . . . . . 6  |-  ( ph  ->  ( ( 0 [,] 1 )  X.  {
( M `  1
) } )  e.  ( II  Cn  C
) )
219 opelxpi 4871 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  ->  <. 1 ,  s
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
22092, 219mpan 670 . . . . . . . . . . . . 13  |-  ( s  e.  ( 0 [,] 1 )  ->  <. 1 ,  s >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
221 fvco3 5768 . . . . . . . . . . . . 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 477 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. 1 ,  s >. )  =  ( F `  ( A `
 <. 1 ,  s
>. ) ) )
22329fveq1d 5693 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  A
) `  <. 1 ,  s >. )  =  ( K `  <. 1 ,  s >. )
)
224222, 223eqtr3d 2477 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( A `  <. 1 ,  s
>. ) )  =  ( K `  <. 1 ,  s >. )
)
225 df-ov 6094 . . . . . . . . . . . 12  |-  ( 1 A s )  =  ( A `  <. 1 ,  s >. )
226225fveq2i 5694 . . . . . . . . . . 11  |-  ( F `
 ( 1 A s ) )  =  ( F `  ( A `  <. 1 ,  s >. ) )
227 df-ov 6094 . . . . . . . . . . 11  |-  ( 1 K s )  =  ( K `  <. 1 ,  s >. )
228224, 226, 2273eqtr4g 2500 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( 1 A s ) )  =  ( 1 K s ) )
229129simprd 463 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
1 K s )  =  ( G ` 
1 ) )
2307simp2d 1001 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  o.  M
)  =  G )
231230adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F  o.  M )  =  G )
232231fveq1d 5693 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  M
) `  1 )  =  ( G ` 
1 ) )
23383adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  M : ( 0 [,] 1 ) --> B )
234 fvco3 5768 . . . . . . . . . . . 12  |-  ( ( M : ( 0 [,] 1 ) --> B  /\  1  e.  ( 0 [,] 1 ) )  ->  ( ( F  o.  M ) `  1 )  =  ( F `  ( M `  1 )
) )
235233, 92, 234sylancl 662 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
( F  o.  M
) `  1 )  =  ( F `  ( M `  1 ) ) )
236232, 235eqtr3d 2477 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( G `  1 )  =  ( F `  ( M `  1 ) ) )
237228, 229, 2363eqtrd 2479 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  ( F `  ( 1 A s ) )  =  ( F `  ( M `  1 ) ) )
238237mpteq2dva 4378 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
1 A s ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( M `
 1 ) ) ) )
239 fconstmpt 4882 . . . . . . . 8  |-  ( ( 0 [,] 1 )  X.  { ( F `
 ( M ` 
1 ) ) } )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `
 ( M ` 
1 ) ) )
240238, 239syl6eqr 2493 . . . . . . 7  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( F `  (
1 A s ) ) )  =  ( ( 0 [,] 1
)  X.  { ( F `  ( M `
 1 ) ) } ) )
241 fovrn 6233 . . . . . . . . . 10  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  1  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  ->  ( 1 A s )  e.  B )
24292, 241mp3an2 1302 . . . . . . . . 9  |-  ( ( A : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B  /\  s  e.  ( 0 [,] 1 ) )  ->  ( 1 A s )  e.  B )
24322, 242sylan 471 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
1 A s )  e.  B )
244 eqidd 2444 . . . . . . . 8  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) ) )
245 fveq2 5691 . . . . . . . 8  |-  ( x  =  ( 1 A s )  ->  ( F `  x )  =  ( F `  ( 1 A s ) ) )
246243, 244, 53, 245fmptco 5876 . . . . . . 7  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( F `  ( 1 A s ) ) ) )
247 fcoconst 5880 . . . . . . . 8  |-  ( ( F  Fn  B  /\  ( M `  1 )  e.  B )  -> 
( F  o.  (
( 0 [,] 1
)  X.  { ( M `  1 ) } ) )  =  ( ( 0 [,] 1 )  X.  {
( F `  ( M `  1 )
) } ) )
248157, 216, 247syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( F  o.  (
( 0 [,] 1
)  X.  { ( M `  1 ) } ) )  =  ( ( 0 [,] 1 )  X.  {
( F `  ( M `  1 )
) } ) )
249240, 246, 2483eqtr4d 2485 . . . . . 6  |-  ( ph  ->  ( F  o.  (
s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) ) )  =  ( F  o.  ( ( 0 [,] 1 )  X.  { ( M `
 1 ) } ) ) )
250 oveq1 6098 . . . . . . . . . 10  |-  ( s  =  1  ->  (
s A 0 )  =  ( 1 A 0 ) )
251 fveq2 5691 . . . . . . . . . 10  |-  ( s  =  1  ->  ( M `  s )  =  ( M ` 
1 ) )
252250, 251eqeq12d 2457 . . . . . . . . 9  |-  ( s  =  1  ->  (
( s A 0 )  =  ( M `
 s )  <->  ( 1 A 0 )  =  ( M `  1
) ) )
253252rspcv 3069 . . . . . . . 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 6099 . . . . . . . . 9  |-  ( s  =  0  ->  (
1 A s )  =  ( 1 A 0 ) )
256 eqid 2443 . . . . . . . . 9  |-  ( s  e.  ( 0 [,] 1 )  |->  ( 1 A s ) )  =  ( s  e.  ( 0 [,] 1
)  |->  ( 1 A s ) )
257 ovex 6116 . . . . . . . . 9  |-  ( 1 A 0 )  e. 
_V
258255, 256, 257fvmpt 5774 . . . . . . . 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 5701 . . . . . . . . 9  |-  ( M `
 1 )  e. 
_V
261260fvconst2 5933 . . . . . . . 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 2500 . . . . . 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 27172 . . . . 5  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) )  =  ( ( 0 [,] 1
)  X.  { ( M `  1 ) } ) )
265 fconstmpt 4882 . . . . 5  |-  ( ( 0 [,] 1 )  X.  { ( M `
 1 ) } )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `
 1 ) )
266264, 265syl6eq 2491 . . . 4  |-  ( ph  ->  ( s  e.  ( 0 [,] 1 ) 
|->  ( 1 A s ) )  =  ( s  e.  ( 0 [,] 1 )  |->  ( M `  1 ) ) )
267 mpteqb 5788 . . . . 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 6116 . . . . . 6  |-  ( 1 A s )  e. 
_V
269268a1i 11 . . . . 5  |-  ( s  e.  ( 0 [,] 1 )  ->  (
1 A s )  e.  _V )
270267, 269mprg 2785 . . . 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 2814 . 2  |-  ( (
ph  /\  s  e.  ( 0 [,] 1
) )  ->  (
1 A s )  =  ( M ` 
1 ) )
2738, 16, 17, 91, 212, 213, 272isphtpy2d 20559 1  |-  ( ph  ->  A  e.  ( M ( PHtpy `  C ) N ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2715   E!wreu 2717   _Vcvv 2972   {csn 3877   <.cop 3883   U.cuni 4091    e. cmpt 4350    X. cxp 4838    o. ccom 4844    Fn wfn 5413   -->wf 5414   ` cfv 5418   iota_crio 6051  (class class class)co 6091   0cc0 9282   1c1 9283   [,]cicc 11303   Topctop 18498  TopOnctopon 18499    Cn ccn 18828   Conccon 19015  𝑛Locally cnlly 19069    tX ctx 19133   IIcii 20451   Htpy chtpy 20539   PHtpycphtpy 20540   CovMap ccvm 27144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-inf2 7847  ax-cnex 9338  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358  ax-pre-mulgt0 9359  ax-pre-sup 9360  ax-addf 9361  ax-mulf 9362
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-reu 2722  df-rmo 2723  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-iin 4174  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-se 4680  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-isom 5427  df-riota 6052  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-of 6320  df-om 6477  df-1st 6577  df-2nd 6578  df-supp 6691  df-recs 6832  df-rdg 6866  df-1o 6920  df-2o 6921  df-oadd 6924  df-er 7101  df-ec 7103  df-map 7216  df-ixp 7264  df-en 7311  df-dom 7312  df-sdom 7313  df-fin 7314  df-fsupp 7621  df-fi 7661  df-sup 7691  df-oi 7724  df-card 8109  df-cda 8337  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424  df-sub 9597  df-neg 9598  df-div 9994  df-nn 10323  df-2 10380  df-3 10381  df-4 10382  df-5 10383  df-6 10384  df-7 10385  df-8 10386  df-9 10387  df-10 10388  df-n0 10580  df-z 10647  df-dec 10756  df-uz 10862  df-q 10954  df-rp 10992  df-xneg 11089  df-xadd 11090  df-xmul 11091  df-ioo 11304  df-ico 11306  df-icc 11307  df-fz 11438  df-fzo 11549  df-fl 11642  df-seq 11807  df-exp 11866  df-hash 12104  df-cj 12588  df-re 12589  df-im 12590  df-sqr 12724  df-abs 12725  df-clim 12966  df-sum 13164  df-struct 14176  df-ndx 14177  df-slot 14178  df-base 14179  df-sets 14180  df-ress 14181  df-plusg 14251  df-mulr 14252  df-starv 14253  df-sca 14254  df-vsca 14255  df-ip 14256  df-tset 14257  df-ple 14258  df-ds 14260  df-unif 14261  df-hom 14262  df-cco 14263  df-rest 14361  df-topn 14362  df-0g 14380  df-gsum 14381  df-topgen 14382  df-pt 14383  df-prds 14386  df-xrs 14440  df-qtop 14445  df-imas 14446  df-xps 14448  df-mre 14524  df-mrc 14525  df-acs 14527  df-mnd 15415  df-submnd 15465  df-mulg 15548  df-cntz 15835  df-cmn 16279  df-psmet 17809  df-xmet 17810  df-met 17811  df-bl 17812  df-mopn 17813  df-cnfld 17819  df-top 18503  df-bases 18505  df-topon 18506  df-topsp 18507  df-cld 18623  df-ntr 18624  df-cls 18625  df-nei 18702  df-cn 18831  df-cnp 18832  df-cmp 18990  df-con 19016  df-lly 19070  df-nlly 19071  df-tx 19135  df-hmeo 19328  df-xms 19895  df-ms 19896  df-tms 19897  df-ii 20453  df-htpy 20542  df-phtpy 20543  df-phtpc 20564  df-pcon 27110  df-scon 27111  df-cvm 27145
This theorem is referenced by:  cvmliftpht  27207
  Copyright terms: Public domain W3C validator