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

Theorem cvmlift2lem12 23860
Description: Lemma for cvmlift2 23862. (Contributed by Mario Carneiro, 1-Jun-2015.)
Hypotheses
Ref Expression
cvmlift2.b  |-  B  = 
U. C
cvmlift2.f  |-  ( ph  ->  F  e.  ( C CovMap  J ) )
cvmlift2.g  |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )
cvmlift2.p  |-  ( ph  ->  P  e.  B )
cvmlift2.i  |-  ( ph  ->  ( F `  P
)  =  ( 0 G 0 ) )
cvmlift2.h  |-  H  =  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) )  /\  ( f `
 0 )  =  P ) )
cvmlift2.k  |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 ) 
|->  ( ( iota_ f  e.  ( II  Cn  C
) ( ( F  o.  f )  =  ( z  e.  ( 0 [,] 1 ) 
|->  ( x G z ) )  /\  (
f `  0 )  =  ( H `  x ) ) ) `
 y ) )
cvmlift2.m  |-  M  =  { z  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) )  |  K  e.  ( ( ( II  tX  II )  CnP  C ) `
 z ) }
cvmlift2.a  |-  A  =  { a  e.  ( 0 [,] 1 )  |  ( ( 0 [,] 1 )  X. 
{ a } ) 
C_  M }
cvmlift2.s  |-  S  =  { <. r ,  t
>.  |  ( t  e.  ( 0 [,] 1
)  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) }
Assertion
Ref Expression
cvmlift2lem12  |-  ( ph  ->  K  e.  ( ( II  tX  II )  Cn  C ) )
Distinct variable groups:    u, f, x, y, z, F    f,
a, r, t, u, x, y, z, ph    A, a, t, x    M, a, r, u, x, y, z    S, f, t, u, x, y, z    f, J, u, x, y, z    G, a, f, t, u, x, y, z    f, H, u, x, y, z    C, a, f, r, t, u, x, y, z    P, f, u, x, y, z    x, B, y, z    K, a, f, r, t, u, x, y, z
Allowed substitution hints:    A( y, z, u, f, r)    B( u, t, f, r, a)    P( t, r, a)    S( r, a)    F( t, r, a)    G( r)    H( t, r, a)    J( t, r, a)    M( t, f)

Proof of Theorem cvmlift2lem12
Dummy variables  b 
c  d  k  s  v  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmlift2.b . . 3  |-  B  = 
U. C
2 cvmlift2.f . . 3  |-  ( ph  ->  F  e.  ( C CovMap  J ) )
3 cvmlift2.g . . 3  |-  ( ph  ->  G  e.  ( ( II  tX  II )  Cn  J ) )
4 cvmlift2.p . . 3  |-  ( ph  ->  P  e.  B )
5 cvmlift2.i . . 3  |-  ( ph  ->  ( F `  P
)  =  ( 0 G 0 ) )
6 cvmlift2.h . . 3  |-  H  =  ( iota_ f  e.  ( II  Cn  C ) ( ( F  o.  f )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) )  /\  ( f `
 0 )  =  P ) )
7 cvmlift2.k . . 3  |-  K  =  ( x  e.  ( 0 [,] 1 ) ,  y  e.  ( 0 [,] 1 ) 
|->  ( ( iota_ f  e.  ( II  Cn  C
) ( ( F  o.  f )  =  ( z  e.  ( 0 [,] 1 ) 
|->  ( x G z ) )  /\  (
f `  0 )  =  ( H `  x ) ) ) `
 y ) )
81, 2, 3, 4, 5, 6, 7cvmlift2lem5 23853 . 2  |-  ( ph  ->  K : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B )
9 iunid 3973 . . . . . . 7  |-  U_ a  e.  ( 0 [,] 1
) { a }  =  ( 0 [,] 1 )
109xpeq2i 4726 . . . . . 6  |-  ( ( 0 [,] 1 )  X.  U_ a  e.  ( 0 [,] 1
) { a } )  =  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )
11 xpiundi 4759 . . . . . 6  |-  ( ( 0 [,] 1 )  X.  U_ a  e.  ( 0 [,] 1
) { a } )  =  U_ a  e.  ( 0 [,] 1
) ( ( 0 [,] 1 )  X. 
{ a } )
1210, 11eqtr3i 2318 . . . . 5  |-  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )  = 
U_ a  e.  ( 0 [,] 1 ) ( ( 0 [,] 1 )  X.  {
a } )
13 cvmlift2.a . . . . . . . 8  |-  A  =  { a  e.  ( 0 [,] 1 )  |  ( ( 0 [,] 1 )  X. 
{ a } ) 
C_  M }
14 iiuni 18401 . . . . . . . . 9  |-  ( 0 [,] 1 )  = 
U. II
15 iicon 18407 . . . . . . . . . 10  |-  II  e.  Con
1615a1i 10 . . . . . . . . 9  |-  ( ph  ->  II  e.  Con )
17 inss1 3402 . . . . . . . . . 10  |-  ( II 
i^i  ( Clsd `  II ) )  C_  II
18 iicmp 18406 . . . . . . . . . . . . . . 15  |-  II  e.  Comp
1918a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  II  e.  Comp )
20 iitop 18400 . . . . . . . . . . . . . . 15  |-  II  e.  Top
2120a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  II  e.  Top )
2220, 20txtopi 17301 . . . . . . . . . . . . . . . 16  |-  ( II 
tX  II )  e. 
Top
2314neiss2 16854 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( II  e.  Top  /\  u  e.  ( ( nei `  II ) `  { r } ) )  ->  { r }  C_  ( 0 [,] 1 ) )
2420, 23mpan 651 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  e.  ( ( nei `  II ) `  {
r } )  ->  { r }  C_  ( 0 [,] 1
) )
25 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  r  e. 
_V
2625snss 3761 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( r  e.  ( 0 [,] 1 )  <->  { r }  C_  ( 0 [,] 1 ) )
2724, 26sylibr 203 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  e.  ( ( nei `  II ) `  {
r } )  -> 
r  e.  ( 0 [,] 1 ) )
2827a1d 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  e.  ( ( nei `  II ) `  {
r } )  -> 
( ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M )  -> 
r  e.  ( 0 [,] 1 ) ) )
2928rexlimiv 2674 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M )  -> 
r  e.  ( 0 [,] 1 ) )
3029adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) )  ->  r  e.  ( 0 [,] 1 ) )
31 simpl 443 . . . . . . . . . . . . . . . . . . 19  |-  ( ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) )  ->  t  e.  ( 0 [,] 1 ) )
3230, 31jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) )  ->  ( r  e.  ( 0 [,] 1
)  /\  t  e.  ( 0 [,] 1
) ) )
3332ssopab2i 4308 . . . . . . . . . . . . . . . . 17  |-  { <. r ,  t >.  |  ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) ) }  C_  { <. r ,  t >.  |  ( r  e.  ( 0 [,] 1 )  /\  t  e.  ( 0 [,] 1 ) ) }
34 cvmlift2.s . . . . . . . . . . . . . . . . 17  |-  S  =  { <. r ,  t
>.  |  ( t  e.  ( 0 [,] 1
)  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) }
35 df-xp 4711 . . . . . . . . . . . . . . . . 17  |-  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )  =  { <. r ,  t
>.  |  ( r  e.  ( 0 [,] 1
)  /\  t  e.  ( 0 [,] 1
) ) }
3633, 34, 353sstr4i 3230 . . . . . . . . . . . . . . . 16  |-  S  C_  ( ( 0 [,] 1 )  X.  (
0 [,] 1 ) )
3720, 20, 14, 14txunii 17304 . . . . . . . . . . . . . . . . 17  |-  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )  = 
U. ( II  tX  II )
3837ntropn 16802 . . . . . . . . . . . . . . . 16  |-  ( ( ( II  tX  II )  e.  Top  /\  S  C_  ( ( 0 [,] 1 )  X.  (
0 [,] 1 ) ) )  ->  (
( int `  (
II  tX  II )
) `  S )  e.  ( II  tX  II ) )
3922, 36, 38mp2an 653 . . . . . . . . . . . . . . 15  |-  ( ( int `  ( II 
tX  II ) ) `
 S )  e.  ( II  tX  II )
4039a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  (
( int `  (
II  tX  II )
) `  S )  e.  ( II  tX  II ) )
412adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  F  e.  ( C CovMap  J ) )
423adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  G  e.  ( (
II  tX  II )  Cn  J ) )
434adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  P  e.  B )
445adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  -> 
( F `  P
)  =  ( 0 G 0 ) )
45 eqid 2296 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/) } )  |  ( U. s  =  ( `' F "
k )  /\  A. c  e.  s  ( A. d  e.  (
s  \  { c } ) ( c  i^i  d )  =  (/)  /\  ( F  |`  c )  e.  ( ( Ct  c )  Homeo  ( Jt  k ) ) ) ) } )  =  ( k  e.  J  |->  { s  e.  ( ~P C  \  { (/)
} )  |  ( U. s  =  ( `' F " k )  /\  A. c  e.  s  ( A. d  e.  ( s  \  {
c } ) ( c  i^i  d )  =  (/)  /\  ( F  |`  c )  e.  ( ( Ct  c ) 
Homeo  ( Jt  k ) ) ) ) } )
46 simprr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  -> 
b  e.  ( 0 [,] 1 ) )
47 simprl 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  -> 
a  e.  ( 0 [,] 1 ) )
481, 41, 42, 43, 44, 6, 7, 45, 46, 47cvmlift2lem10 23858 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  E. u  e.  II  E. v  e.  II  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v  ( K  |`  ( u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )
4922a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  ( II  tX  II )  e.  Top )
5036a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  S  C_  (
( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
5120a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  II  e.  Top )
52 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  u  e.  II )
53 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  v  e.  II )
54 txopn 17313 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( II  e.  Top  /\  II  e.  Top )  /\  ( u  e.  II  /\  v  e.  II ) )  ->  (
u  X.  v )  e.  ( II  tX  II ) )
5551, 51, 52, 53, 54syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  ( u  X.  v )  e.  ( II  tX  II )
)
56 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( r  e.  u  /\  t  e.  v )  ->  t  e.  v )
57 elunii 3848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( t  e.  v  /\  v  e.  II )  ->  t  e.  U. II )
5857, 14syl6eleqr 2387 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( t  e.  v  /\  v  e.  II )  ->  t  e.  ( 0 [,] 1 ) )
5956, 53, 58syl2anr 464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
t  e.  ( 0 [,] 1 ) )
6020a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  ->  II  e.  Top )
6152adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  ->  u  e.  II )
62 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
r  e.  u )
63 opnneip 16872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( II  e.  Top  /\  u  e.  II  /\  r  e.  u )  ->  u  e.  ( ( nei `  II ) `
 { r } ) )
6460, 61, 62, 63syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  ->  u  e.  ( ( nei `  II ) `  { r } ) )
6541ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  ->  F  e.  ( C CovMap  J ) )
6642ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  ->  G  e.  ( (
II  tX  II )  Cn  J ) )
6743ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  ->  P  e.  B )
6844ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
( F `  P
)  =  ( 0 G 0 ) )
69 cvmlift2.m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  M  =  { z  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) )  |  K  e.  ( ( ( II  tX  II )  CnP  C ) `
 z ) }
7053adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
v  e.  II )
71 simplr2 998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
a  e.  v )
72 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
t  e.  v )
73 sneq 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  w  ->  { c }  =  { w } )
7473xpeq2d 4729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  w  ->  (
u  X.  { c } )  =  ( u  X.  { w } ) )
7574reseq2d 4971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( c  =  w  ->  ( K  |`  ( u  X.  { c } ) )  =  ( K  |`  ( u  X.  {
w } ) ) )
7674oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  w  ->  (
( II  tX  II )t  ( u  X.  { c } ) )  =  ( ( II  tX  II )t  ( u  X.  { w } ) ) )
7776oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( c  =  w  ->  (
( ( II  tX  II )t  ( u  X.  { c } ) )  Cn  C )  =  ( ( ( II  tX  II )t  (
u  X.  { w } ) )  Cn  C ) )
7875, 77eleq12d 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( c  =  w  ->  (
( K  |`  (
u  X.  { c } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { c } ) )  Cn  C
)  <->  ( K  |`  ( u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
) ) )
7978cbvrexv 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( E. c  e.  v  ( K  |`  ( u  X.  { c } ) )  e.  ( ( ( II  tX  II )t  ( u  X.  { c } ) )  Cn  C )  <->  E. w  e.  v  ( K  |`  ( u  X.  {
w } ) )  e.  ( ( ( II  tX  II )t  (
u  X.  { w } ) )  Cn  C ) )
80 simplr3 999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
( E. w  e.  v  ( K  |`  ( u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) )
8179, 80syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
( E. c  e.  v  ( K  |`  ( u  X.  { c } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { c } ) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) )
821, 65, 66, 67, 68, 6, 7, 69, 61, 70, 71, 72, 81cvmlift2lem11 23859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
( ( u  X.  { a } ) 
C_  M  ->  (
u  X.  { t } )  C_  M
) )
831, 65, 66, 67, 68, 6, 7, 69, 61, 70, 72, 71, 81cvmlift2lem11 23859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
( ( u  X.  { t } ) 
C_  M  ->  (
u  X.  { a } )  C_  M
) )
8482, 83impbid 183 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
( ( u  X.  { a } ) 
C_  M  <->  ( u  X.  { t } ) 
C_  M ) )
85 rspe 2617 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( u  e.  ( ( nei `  II ) `
 { r } )  /\  ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) )  ->  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) )
8664, 84, 85syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  ->  E. u  e.  (
( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) )
8759, 86jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  /\  ( r  e.  u  /\  t  e.  v ) )  -> 
( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) )
8887ex 423 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  ( (
r  e.  u  /\  t  e.  v )  ->  ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) ) )
8988alrimivv 1622 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  A. r A. t ( ( r  e.  u  /\  t  e.  v )  ->  (
t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) ) ) )
90 df-xp 4711 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( u  X.  v )  =  { <. r ,  t
>.  |  ( r  e.  u  /\  t  e.  v ) }
9190, 34sseq12i 3217 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( u  X.  v ) 
C_  S  <->  { <. r ,  t >.  |  ( r  e.  u  /\  t  e.  v ) }  C_  { <. r ,  t >.  |  ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) ) } )
92 ssopab2b 4307 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( {
<. r ,  t >.  |  ( r  e.  u  /\  t  e.  v ) }  C_  {
<. r ,  t >.  |  ( t  e.  ( 0 [,] 1
)  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) }  <->  A. r A. t ( ( r  e.  u  /\  t  e.  v )  ->  (
t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) ) ) )
9391, 92bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( u  X.  v ) 
C_  S  <->  A. r A. t ( ( r  e.  u  /\  t  e.  v )  ->  (
t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) ) ) )
9489, 93sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  ( u  X.  v )  C_  S
)
9537ssntr 16811 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( II  tX  II )  e.  Top  /\  S  C_  ( (
0 [,] 1 )  X.  ( 0 [,] 1 ) ) )  /\  ( ( u  X.  v )  e.  ( II  tX  II )  /\  ( u  X.  v )  C_  S
) )  ->  (
u  X.  v ) 
C_  ( ( int `  ( II  tX  II ) ) `  S
) )
9649, 50, 55, 94, 95syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  ( u  X.  v )  C_  (
( int `  (
II  tX  II )
) `  S )
)
97 simpr1 961 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  b  e.  u )
98 simpr2 962 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  a  e.  v )
99 opelxpi 4737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  e.  u  /\  a  e.  v )  -> 
<. b ,  a >.  e.  ( u  X.  v
) )
10097, 98, 99syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  <. b ,  a >.  e.  (
u  X.  v ) )
10196, 100sseldd 3194 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  (
u  e.  II  /\  v  e.  II )
)  /\  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )  ->  <. b ,  a >.  e.  (
( int `  (
II  tX  II )
) `  S )
)
102101ex 423 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
a  e.  ( 0 [,] 1 )  /\  b  e.  ( 0 [,] 1 ) ) )  /\  ( u  e.  II  /\  v  e.  II ) )  -> 
( ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v  ( K  |`  ( u  X.  { w } ) )  e.  ( ( ( II  tX  II )t  ( u  X.  { w } ) )  Cn  C )  ->  ( K  |`  ( u  X.  v ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  v ) )  Cn  C ) ) )  ->  <. b ,  a >.  e.  (
( int `  (
II  tX  II )
) `  S )
) )
103102rexlimdvva 2687 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  -> 
( E. u  e.  II  E. v  e.  II  ( b  e.  u  /\  a  e.  v  /\  ( E. w  e.  v  ( K  |`  ( u  X.  { w } ) )  e.  ( ( ( II  tX  II )t  ( u  X.  { w } ) )  Cn  C )  ->  ( K  |`  ( u  X.  v ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  v ) )  Cn  C ) ) )  ->  <. b ,  a >.  e.  (
( int `  (
II  tX  II )
) `  S )
) )
10448, 103mpd 14 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  <. b ,  a >.  e.  ( ( int `  (
II  tX  II )
) `  S )
)
105 vex 2804 . . . . . . . . . . . . . . . . . . 19  |-  a  e. 
_V
106 opeq2 3813 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  a  ->  <. b ,  w >.  =  <. b ,  a >. )
107106eleq1d 2362 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  a  ->  ( <. b ,  w >.  e.  ( ( int `  (
II  tX  II )
) `  S )  <->  <.
b ,  a >.  e.  ( ( int `  (
II  tX  II )
) `  S )
) )
108105, 107ralsn 3687 . . . . . . . . . . . . . . . . . 18  |-  ( A. w  e.  { a } <. b ,  w >.  e.  ( ( int `  ( II  tX  II ) ) `  S
)  <->  <. b ,  a
>.  e.  ( ( int `  ( II  tX  II ) ) `  S
) )
109104, 108sylibr 203 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  A. w  e.  { a } <. b ,  w >.  e.  ( ( int `  ( II  tX  II ) ) `  S
) )
110109anassrs 629 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  a  e.  ( 0 [,] 1
) )  /\  b  e.  ( 0 [,] 1
) )  ->  A. w  e.  { a } <. b ,  w >.  e.  ( ( int `  (
II  tX  II )
) `  S )
)
111110ralrimiva 2639 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  A. b  e.  ( 0 [,] 1
) A. w  e. 
{ a } <. b ,  w >.  e.  ( ( int `  (
II  tX  II )
) `  S )
)
112 dfss3 3183 . . . . . . . . . . . . . . . 16  |-  ( ( ( 0 [,] 1
)  X.  { a } )  C_  (
( int `  (
II  tX  II )
) `  S )  <->  A. u  e.  ( ( 0 [,] 1 )  X.  { a } ) u  e.  ( ( int `  (
II  tX  II )
) `  S )
)
113 eleq1 2356 . . . . . . . . . . . . . . . . 17  |-  ( u  =  <. b ,  w >.  ->  ( u  e.  ( ( int `  (
II  tX  II )
) `  S )  <->  <.
b ,  w >.  e.  ( ( int `  (
II  tX  II )
) `  S )
) )
114113ralxp 4843 . . . . . . . . . . . . . . . 16  |-  ( A. u  e.  ( (
0 [,] 1 )  X.  { a } ) u  e.  ( ( int `  (
II  tX  II )
) `  S )  <->  A. b  e.  ( 0 [,] 1 ) A. w  e.  { a } <. b ,  w >.  e.  ( ( int `  ( II  tX  II ) ) `  S
) )
115112, 114bitri 240 . . . . . . . . . . . . . . 15  |-  ( ( ( 0 [,] 1
)  X.  { a } )  C_  (
( int `  (
II  tX  II )
) `  S )  <->  A. b  e.  ( 0 [,] 1 ) A. w  e.  { a } <. b ,  w >.  e.  ( ( int `  ( II  tX  II ) ) `  S
) )
116111, 115sylibr 203 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  (
( 0 [,] 1
)  X.  { a } )  C_  (
( int `  (
II  tX  II )
) `  S )
)
117 simpr 447 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  a  e.  ( 0 [,] 1
) )
11814, 14, 19, 21, 40, 116, 117txtube 17350 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  E. v  e.  II  ( a  e.  v  /\  ( ( 0 [,] 1 )  X.  v )  C_  ( ( int `  (
II  tX  II )
) `  S )
) )
11937ntrss2 16810 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( II  tX  II )  e.  Top  /\  S  C_  ( ( 0 [,] 1 )  X.  (
0 [,] 1 ) ) )  ->  (
( int `  (
II  tX  II )
) `  S )  C_  S )
12022, 36, 119mp2an 653 . . . . . . . . . . . . . . . . . 18  |-  ( ( int `  ( II 
tX  II ) ) `
 S )  C_  S
121 sstr 3200 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 0 [,] 1 )  X.  v
)  C_  ( ( int `  ( II  tX  II ) ) `  S
)  /\  ( ( int `  ( II  tX  II ) ) `  S
)  C_  S )  ->  ( ( 0 [,] 1 )  X.  v
)  C_  S )
122120, 121mpan2 652 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 0 [,] 1
)  X.  v ) 
C_  ( ( int `  ( II  tX  II ) ) `  S
)  ->  ( (
0 [,] 1 )  X.  v )  C_  S )
123 df-xp 4711 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0 [,] 1 )  X.  v )  =  { <. r ,  t
>.  |  ( r  e.  ( 0 [,] 1
)  /\  t  e.  v ) }
124123, 34sseq12i 3217 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 0 [,] 1
)  X.  v ) 
C_  S  <->  { <. r ,  t >.  |  ( r  e.  ( 0 [,] 1 )  /\  t  e.  v ) }  C_  { <. r ,  t >.  |  ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) ) } )
125 ssopab2b 4307 . . . . . . . . . . . . . . . . . . 19  |-  ( {
<. r ,  t >.  |  ( r  e.  ( 0 [,] 1
)  /\  t  e.  v ) }  C_  {
<. r ,  t >.  |  ( t  e.  ( 0 [,] 1
)  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) }  <->  A. r A. t ( ( r  e.  ( 0 [,] 1 )  /\  t  e.  v )  ->  (
t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) ) ) )
126 r2al 2593 . . . . . . . . . . . . . . . . . . 19  |-  ( A. r  e.  ( 0 [,] 1 ) A. t  e.  v  (
t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) )  <->  A. r A. t ( ( r  e.  ( 0 [,] 1 )  /\  t  e.  v )  ->  ( t  e.  ( 0 [,] 1
)  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) ) )
127 ralcom 2713 . . . . . . . . . . . . . . . . . . 19  |-  ( A. r  e.  ( 0 [,] 1 ) A. t  e.  v  (
t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) )  <->  A. t  e.  v  A. r  e.  (
0 [,] 1 ) ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) )
128125, 126, 1273bitr2i 264 . . . . . . . . . . . . . . . . . 18  |-  ( {
<. r ,  t >.  |  ( r  e.  ( 0 [,] 1
)  /\  t  e.  v ) }  C_  {
<. r ,  t >.  |  ( t  e.  ( 0 [,] 1
)  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) }  <->  A. t  e.  v  A. r  e.  ( 0 [,] 1
) ( t  e.  ( 0 [,] 1
)  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) )
129124, 128bitri 240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 0 [,] 1
)  X.  v ) 
C_  S  <->  A. t  e.  v  A. r  e.  ( 0 [,] 1
) ( t  e.  ( 0 [,] 1
)  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) )
130122, 129sylib 188 . . . . . . . . . . . . . . . 16  |-  ( ( ( 0 [,] 1
)  X.  v ) 
C_  ( ( int `  ( II  tX  II ) ) `  S
)  ->  A. t  e.  v  A. r  e.  ( 0 [,] 1
) ( t  e.  ( 0 [,] 1
)  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) ) )
131 simpr 447 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) )  ->  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) )
132131ralimi 2631 . . . . . . . . . . . . . . . . . . 19  |-  ( A. r  e.  ( 0 [,] 1 ) ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) )  ->  A. r  e.  ( 0 [,] 1 ) E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) )
133 cvmlift2lem1 23848 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. r  e.  ( 0 [,] 1 ) E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M )  -> 
( ( ( 0 [,] 1 )  X. 
{ a } ) 
C_  M  ->  (
( 0 [,] 1
)  X.  { t } )  C_  M
) )
134 bicom 191 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( u  X.  {
a } )  C_  M 
<->  ( u  X.  {
t } )  C_  M )  <->  ( (
u  X.  { t } )  C_  M  <->  ( u  X.  { a } )  C_  M
) )
135134rexbii 2581 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M )  <->  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { t } )  C_  M  <->  ( u  X.  { a } )  C_  M
) )
136135ralbii 2580 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. r  e.  ( 0 [,] 1 ) E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M )  <->  A. r  e.  ( 0 [,] 1
) E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { t } )  C_  M  <->  ( u  X.  { a } )  C_  M
) )
137 cvmlift2lem1 23848 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. r  e.  ( 0 [,] 1 ) E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { t } )  C_  M  <->  ( u  X.  { a } ) 
C_  M )  -> 
( ( ( 0 [,] 1 )  X. 
{ t } ) 
C_  M  ->  (
( 0 [,] 1
)  X.  { a } )  C_  M
) )
138136, 137sylbi 187 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. r  e.  ( 0 [,] 1 ) E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M )  -> 
( ( ( 0 [,] 1 )  X. 
{ t } ) 
C_  M  ->  (
( 0 [,] 1
)  X.  { a } )  C_  M
) )
139133, 138impbid 183 . . . . . . . . . . . . . . . . . . 19  |-  ( A. r  e.  ( 0 [,] 1 ) E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M )  -> 
( ( ( 0 [,] 1 )  X. 
{ a } ) 
C_  M  <->  ( (
0 [,] 1 )  X.  { t } )  C_  M )
)
140132, 139syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( A. r  e.  ( 0 [,] 1 ) ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) )  ->  ( ( ( 0 [,] 1 )  X.  { a } )  C_  M  <->  ( (
0 [,] 1 )  X.  { t } )  C_  M )
)
141 simpllr 735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  a  e.  ( 0 [,] 1 ) )  /\  v  e.  II )  /\  t  e.  v )  ->  a  e.  ( 0 [,] 1
) )
14213rabeq2i 2798 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  A  <->  ( a  e.  ( 0 [,] 1
)  /\  ( (
0 [,] 1 )  X.  { a } )  C_  M )
)
143142baib 871 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  ( 0 [,] 1 )  ->  (
a  e.  A  <->  ( (
0 [,] 1 )  X.  { a } )  C_  M )
)
144141, 143syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  a  e.  ( 0 [,] 1 ) )  /\  v  e.  II )  /\  t  e.  v )  ->  ( a  e.  A  <->  ( ( 0 [,] 1 )  X. 
{ a } ) 
C_  M ) )
145 elssuni 3871 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  e.  II  ->  v  C_ 
U. II )
146145, 14syl6sseqr 3238 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  II  ->  v  C_  ( 0 [,] 1
) )
147146adantl 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  a  e.  ( 0 [,] 1
) )  /\  v  e.  II )  ->  v  C_  ( 0 [,] 1
) )
148147sselda 3193 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  a  e.  ( 0 [,] 1 ) )  /\  v  e.  II )  /\  t  e.  v )  ->  t  e.  ( 0 [,] 1
) )
149 sneq 3664 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  t  ->  { a }  =  { t } )
150149xpeq2d 4729 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  t  ->  (
( 0 [,] 1
)  X.  { a } )  =  ( ( 0 [,] 1
)  X.  { t } ) )
151150sseq1d 3218 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  t  ->  (
( ( 0 [,] 1 )  X.  {
a } )  C_  M 
<->  ( ( 0 [,] 1 )  X.  {
t } )  C_  M ) )
152151, 13elrab2 2938 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  A  <->  ( t  e.  ( 0 [,] 1
)  /\  ( (
0 [,] 1 )  X.  { t } )  C_  M )
)
153152baib 871 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  ( 0 [,] 1 )  ->  (
t  e.  A  <->  ( (
0 [,] 1 )  X.  { t } )  C_  M )
)
154148, 153syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  a  e.  ( 0 [,] 1 ) )  /\  v  e.  II )  /\  t  e.  v )  ->  ( t  e.  A  <->  ( ( 0 [,] 1 )  X. 
{ t } ) 
C_  M ) )
155144, 154bibi12d 312 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  a  e.  ( 0 [,] 1 ) )  /\  v  e.  II )  /\  t  e.  v )  ->  ( (
a  e.  A  <->  t  e.  A )  <->  ( (
( 0 [,] 1
)  X.  { a } )  C_  M  <->  ( ( 0 [,] 1
)  X.  { t } )  C_  M
) ) )
156140, 155syl5ibr 212 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  a  e.  ( 0 [,] 1 ) )  /\  v  e.  II )  /\  t  e.  v )  ->  ( A. r  e.  ( 0 [,] 1 ) ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M ) )  ->  ( a  e.  A  <->  t  e.  A
) ) )
157156ralimdva 2634 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  a  e.  ( 0 [,] 1
) )  /\  v  e.  II )  ->  ( A. t  e.  v  A. r  e.  (
0 [,] 1 ) ( t  e.  ( 0 [,] 1 )  /\  E. u  e.  ( ( nei `  II ) `  { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } )  C_  M
) )  ->  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) )
158130, 157syl5 28 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  a  e.  ( 0 [,] 1
) )  /\  v  e.  II )  ->  (
( ( 0 [,] 1 )  X.  v
)  C_  ( ( int `  ( II  tX  II ) ) `  S
)  ->  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) )
159158anim2d 548 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  a  e.  ( 0 [,] 1
) )  /\  v  e.  II )  ->  (
( a  e.  v  /\  ( ( 0 [,] 1 )  X.  v )  C_  (
( int `  (
II  tX  II )
) `  S )
)  ->  ( a  e.  v  /\  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) ) )
160159reximdva 2668 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  ( E. v  e.  II  ( a  e.  v  /\  ( ( 0 [,] 1 )  X.  v )  C_  (
( int `  (
II  tX  II )
) `  S )
)  ->  E. v  e.  II  ( a  e.  v  /\  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) ) )
161118, 160mpd 14 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  E. v  e.  II  ( a  e.  v  /\  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) )
162161ralrimiva 2639 . . . . . . . . . . 11  |-  ( ph  ->  A. a  e.  ( 0 [,] 1 ) E. v  e.  II  ( a  e.  v  /\  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) )
163 ssrab2 3271 . . . . . . . . . . . . 13  |-  { a  e.  ( 0 [,] 1 )  |  ( ( 0 [,] 1
)  X.  { a } )  C_  M }  C_  ( 0 [,] 1 )
16413, 163eqsstri 3221 . . . . . . . . . . . 12  |-  A  C_  ( 0 [,] 1
)
16514isclo 16840 . . . . . . . . . . . 12  |-  ( ( II  e.  Top  /\  A  C_  ( 0 [,] 1 ) )  -> 
( A  e.  ( II  i^i  ( Clsd `  II ) )  <->  A. a  e.  ( 0 [,] 1
) E. v  e.  II  ( a  e.  v  /\  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) ) )
16620, 164, 165mp2an 653 . . . . . . . . . . 11  |-  ( A  e.  ( II  i^i  ( Clsd `  II )
)  <->  A. a  e.  ( 0 [,] 1 ) E. v  e.  II  ( a  e.  v  /\  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) )
167162, 166sylibr 203 . . . . . . . . . 10  |-  ( ph  ->  A  e.  ( II 
i^i  ( Clsd `  II ) ) )
16817, 167sseldi 3191 . . . . . . . . 9  |-  ( ph  ->  A  e.  II )
169 0elunit 10770 . . . . . . . . . . . 12  |-  0  e.  ( 0 [,] 1
)
170169a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( 0 [,] 1 ) )
171 relxp 4810 . . . . . . . . . . . . 13  |-  Rel  (
( 0 [,] 1
)  X.  { 0 } )
172171a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  Rel  ( ( 0 [,] 1 )  X. 
{ 0 } ) )
173 opelxp 4735 . . . . . . . . . . . . 13  |-  ( <.
r ,  a >.  e.  ( ( 0 [,] 1 )  X.  {
0 } )  <->  ( r  e.  ( 0 [,] 1
)  /\  a  e.  { 0 } ) )
174 id 19 . . . . . . . . . . . . . . . . 17  |-  ( r  e.  ( 0 [,] 1 )  ->  r  e.  ( 0 [,] 1
) )
175 opelxpi 4737 . . . . . . . . . . . . . . . . 17  |-  ( ( r  e.  ( 0 [,] 1 )  /\  0  e.  ( 0 [,] 1 ) )  ->  <. r ,  0
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
176174, 170, 175syl2anr 464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  <. r ,  0 >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
1772adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  F  e.  ( C CovMap  J ) )
1783adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  G  e.  ( ( II  tX  II )  Cn  J
) )
1794adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  P  e.  B )
1805adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  ( F `  P )  =  ( 0 G 0 ) )
181 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  r  e.  ( 0 [,] 1
) )
182169a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  0  e.  ( 0 [,] 1
) )
1831, 177, 178, 179, 180, 6, 7, 45, 181, 182cvmlift2lem10 23858 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  E. u  e.  II  E. v  e.  II  ( r  e.  u  /\  0  e.  v  /\  ( E. w  e.  v  ( K  |`  ( u  X.  { w } ) )  e.  ( ( ( II  tX  II )t  ( u  X.  { w } ) )  Cn  C )  ->  ( K  |`  ( u  X.  v ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )
184 df-3an 936 . . . . . . . . . . . . . . . . . . 19  |-  ( ( r  e.  u  /\  0  e.  v  /\  ( E. w  e.  v  ( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) )  <-> 
( ( r  e.  u  /\  0  e.  v )  /\  ( E. w  e.  v 
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) ) )
185 simprr 733 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  0  e.  v )
1868ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  K : ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) --> B )
187 ffn 5405 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( K : ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) --> B  ->  K  Fn  ( (
0 [,] 1 )  X.  ( 0 [,] 1 ) ) )
188186, 187syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  K  Fn  ( ( 0 [,] 1 )  X.  (
0 [,] 1 ) ) )
189 fnov 5968 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( K  Fn  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) )  <->  K  =  ( b  e.  ( 0 [,] 1 ) ,  w  e.  ( 0 [,] 1 ) 
|->  ( b K w ) ) )
190188, 189sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  K  =  ( b  e.  ( 0 [,] 1
) ,  w  e.  ( 0 [,] 1
)  |->  ( b K w ) ) )
191190reseq1d 4970 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  ( K  |`  ( u  X.  { 0 } ) )  =  ( ( b  e.  ( 0 [,] 1 ) ,  w  e.  ( 0 [,] 1 )  |->  ( b K w ) )  |`  ( u  X.  { 0 } ) ) )
192 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  u  e.  II )
193 elssuni 3871 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( u  e.  II  ->  u  C_ 
U. II )
194193, 14syl6sseqr 3238 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( u  e.  II  ->  u  C_  ( 0 [,] 1
) )
195192, 194syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  u  C_  ( 0 [,] 1
) )
196170snssd 3776 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  { 0 }  C_  ( 0 [,] 1
) )
197196ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  { 0 }  C_  ( 0 [,] 1 ) )
198 resmpt2 5958 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( u  C_  ( 0 [,] 1 )  /\  { 0 }  C_  (
0 [,] 1 ) )  ->  ( (
b  e.  ( 0 [,] 1 ) ,  w  e.  ( 0 [,] 1 )  |->  ( b K w ) )  |`  ( u  X.  { 0 } ) )  =  ( b  e.  u ,  w  e.  { 0 }  |->  ( b K w ) ) )
199195, 197, 198syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
( b  e.  ( 0 [,] 1 ) ,  w  e.  ( 0 [,] 1 ) 
|->  ( b K w ) )  |`  (
u  X.  { 0 } ) )  =  ( b  e.  u ,  w  e.  { 0 }  |->  ( b K w ) ) )
200195sselda 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  /\  b  e.  u )  ->  b  e.  ( 0 [,] 1
) )
201 simplll 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  ph )
2021, 2, 3, 4, 5, 6, 7cvmlift2lem8 23856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  b  e.  ( 0 [,] 1
) )  ->  (
b K 0 )  =  ( H `  b ) )
203201, 202sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  /\  b  e.  ( 0 [,] 1
) )  ->  (
b K 0 )  =  ( H `  b ) )
204200, 203syldan 456 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  /\  b  e.  u )  ->  (
b K 0 )  =  ( H `  b ) )
205 elsni 3677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  { 0 }  ->  w  =  0 )
206205oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  e.  { 0 }  ->  ( b K w )  =  ( b K 0 ) )
207206eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  { 0 }  ->  ( ( b K w )  =  ( H `  b
)  <->  ( b K 0 )  =  ( H `  b ) ) )
208204, 207syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  /\  b  e.  u )  ->  (
w  e.  { 0 }  ->  ( b K w )  =  ( H `  b
) ) )
2092083impia 1148 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  /\  b  e.  u  /\  w  e.  { 0 } )  ->  ( b K w )  =  ( H `  b ) )
210209mpt2eq3dva 5928 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
b  e.  u ,  w  e.  { 0 }  |->  ( b K w ) )  =  ( b  e.  u ,  w  e.  { 0 }  |->  ( H `  b ) ) )
211191, 199, 2103eqtrd 2332 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  ( K  |`  ( u  X.  { 0 } ) )  =  ( b  e.  u ,  w  e.  { 0 }  |->  ( H `  b ) ) )
212 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( IIt  u )  =  ( IIt  u )
213 iitopon 18399 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  II  e.  (TopOn `  ( 0 [,] 1 ) )
214213a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  II  e.  (TopOn `  ( 0 [,] 1 ) ) )
215 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( IIt  {
0 } )  =  ( IIt  { 0 } )
216214, 214cnmpt1st 17378 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
b  e.  ( 0 [,] 1 ) ,  w  e.  ( 0 [,] 1 )  |->  b )  e.  ( ( II  tX  II )  Cn  II ) )
2171, 2, 3, 4, 5, 6cvmlift2lem2 23850 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( H  e.  ( II  Cn  C )  /\  ( F  o.  H )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) )  /\  ( H `
 0 )  =  P ) )
218217simp1d 967 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  H  e.  ( II 
Cn  C ) )
219201, 218syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  H  e.  ( II  Cn  C
) )
220214, 214, 216, 219cnmpt21f 17382 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
b  e.  ( 0 [,] 1 ) ,  w  e.  ( 0 [,] 1 )  |->  ( H `  b ) )  e.  ( ( II  tX  II )  Cn  C ) )
221212, 214, 195, 215, 214, 197, 220cnmpt2res 17387 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
b  e.  u ,  w  e.  { 0 }  |->  ( H `  b ) )  e.  ( ( ( IIt  u )  tX  ( IIt  {
0 } ) )  Cn  C ) )
222 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  u  e. 
_V
223 snex 4232 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  { 0 }  e.  _V
224 txrest 17341 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( II  e.  Top  /\  II  e.  Top )  /\  ( u  e.  _V  /\ 
{ 0 }  e.  _V ) )  ->  (
( II  tX  II )t  ( u  X.  { 0 } ) )  =  ( ( IIt  u ) 
tX  ( IIt  { 0 } ) ) )
22520, 20, 222, 223, 224mp4an 654 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( II  tX  II )t  (
u  X.  { 0 } ) )  =  ( ( IIt  u ) 
tX  ( IIt  { 0 } ) )
226225oveq1i 5884 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( II  tX  II )t  ( u  X.  { 0 } ) )  Cn  C )  =  ( ( ( IIt  u ) 
tX  ( IIt  { 0 } ) )  Cn  C )
227221, 226syl6eleqr 2387 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
b  e.  u ,  w  e.  { 0 }  |->  ( H `  b ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { 0 } ) )  Cn  C
) )
228211, 227eqeltrd 2370 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  ( K  |`  ( u  X.  { 0 } ) )  e.  ( ( ( II  tX  II )t  ( u  X.  { 0 } ) )  Cn  C ) )
229 sneq 3664 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  0  ->  { w }  =  { 0 } )
230229xpeq2d 4729 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  0  ->  (
u  X.  { w } )  =  ( u  X.  { 0 } ) )
231230reseq2d 4971 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  0  ->  ( K  |`  ( u  X.  { w } ) )  =  ( K  |`  ( u  X.  {
0 } ) ) )
232230oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  0  ->  (
( II  tX  II )t  ( u  X.  { w } ) )  =  ( ( II  tX  II )t  ( u  X.  { 0 } ) ) )
233232oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  0  ->  (
( ( II  tX  II )t  ( u  X.  { w } ) )  Cn  C )  =  ( ( ( II  tX  II )t  (
u  X.  { 0 } ) )  Cn  C ) )
234231, 233eleq12d 2364 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  0  ->  (
( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  <->  ( K  |`  ( u  X.  { 0 } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { 0 } ) )  Cn  C
) ) )
235234rspcev 2897 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 0  e.  v  /\  ( K  |`  ( u  X.  { 0 } ) )  e.  ( ( ( II  tX  II )t  ( u  X.  { 0 } ) )  Cn  C ) )  ->  E. w  e.  v  ( K  |`  ( u  X.  {
w } ) )  e.  ( ( ( II  tX  II )t  (
u  X.  { w } ) )  Cn  C ) )
236185, 228, 235syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  E. w  e.  v  ( K  |`  ( u  X.  {
w } ) )  e.  ( ( ( II  tX  II )t  (
u  X.  { w } ) )  Cn  C ) )
237 opelxpi 4737 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( r  e.  u  /\  0  e.  v )  -> 
<. r ,  0 >.  e.  ( u  X.  v
) )
238237adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  <. r ,  0 >.  e.  ( u  X.  v ) )
239 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  v  e.  II )
240239, 146syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  v  C_  ( 0 [,] 1
) )
241 xpss12 4808 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( u  C_  ( 0 [,] 1 )  /\  v  C_  ( 0 [,] 1 ) )  -> 
( u  X.  v
)  C_  ( (
0 [,] 1 )  X.  ( 0 [,] 1 ) ) )
242195, 240, 241syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
u  X.  v ) 
C_  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
24337restuni 16909 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( II  tX  II )  e.  Top  /\  (
u  X.  v ) 
C_  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )  -> 
( u  X.  v
)  =  U. (
( II  tX  II )t  ( u  X.  v
) ) )
24422, 242, 243sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
u  X.  v )  =  U. ( ( II  tX  II )t  (
u  X.  v ) ) )
245238, 244eleqtrd 2372 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  <. r ,  0 >.  e.  U. ( ( II  tX  II )t  ( u  X.  v ) ) )
246 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  U. (
( II  tX  II )t  ( u  X.  v
) )  =  U. ( ( II  tX  II )t  ( u  X.  v ) )
247246cncnpi 17023 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( K  |`  (
u  X.  v ) )  e.  ( ( ( II  tX  II )t  ( u  X.  v
) )  Cn  C
)  /\  <. r ,  0 >.  e.  U. (
( II  tX  II )t  ( u  X.  v
) ) )  -> 
( K  |`  (
u  X.  v ) )  e.  ( ( ( ( II  tX  II )t  ( u  X.  v ) )  CnP 
C ) `  <. r ,  0 >. )
)
248247expcom 424 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( <.
r ,  0 >.  e.  U. ( ( II 
tX  II )t  ( u  X.  v ) )  ->  ( ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C )  ->  ( K  |`  ( u  X.  v ) )  e.  ( ( ( ( II  tX  II )t  (
u  X.  v ) )  CnP  C ) `
 <. r ,  0
>. ) ) )
249245, 248syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
( K  |`  (
u  X.  v ) )  e.  ( ( ( II  tX  II )t  ( u  X.  v
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( ( II 
tX  II )t  ( u  X.  v ) )  CnP  C ) `  <. r ,  0 >.
) ) )
25022a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
II  tX  II )  e.  Top )
25120a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  II  e.  Top )
252251, 251, 192, 239, 54syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
u  X.  v )  e.  ( II  tX  II ) )
253 isopn3i 16835 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( II  tX  II )  e.  Top  /\  (
u  X.  v )  e.  ( II  tX  II ) )  ->  (
( int `  (
II  tX  II )
) `  ( u  X.  v ) )  =  ( u  X.  v
) )
25422, 252, 253sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
( int `  (
II  tX  II )
) `  ( u  X.  v ) )  =  ( u  X.  v
) )
255238, 254eleqtrrd 2373 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  <. r ,  0 >.  e.  ( ( int `  (
II  tX  II )
) `  ( u  X.  v ) ) )
25637, 1cnprest 17033 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( II  tX  II )  e.  Top  /\  ( u  X.  v
)  C_  ( (
0 [,] 1 )  X.  ( 0 [,] 1 ) ) )  /\  ( <. r ,  0 >.  e.  ( ( int `  (
II  tX  II )
) `  ( u  X.  v ) )  /\  K : ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) --> B ) )  ->  ( K  e.  ( ( ( II 
tX  II )  CnP 
C ) `  <. r ,  0 >. )  <->  ( K  |`  ( u  X.  v ) )  e.  ( ( ( ( II  tX  II )t  (
u  X.  v ) )  CnP  C ) `
 <. r ,  0
>. ) ) )
257250, 242, 255, 186, 256syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  ( K  e.  ( (
( II  tX  II )  CnP  C ) `  <. r ,  0 >.
)  <->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( ( II 
tX  II )t  ( u  X.  v ) )  CnP  C ) `  <. r ,  0 >.
) ) )
258249, 257sylibrd 225 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
( K  |`  (
u  X.  v ) )  e.  ( ( ( II  tX  II )t  ( u  X.  v
) )  Cn  C
)  ->  K  e.  ( ( ( II 
tX  II )  CnP 
C ) `  <. r ,  0 >. )
) )
259236, 258embantd 50 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
( E. w  e.  v  ( K  |`  ( u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) )  ->  K  e.  ( (
( II  tX  II )  CnP  C ) `  <. r ,  0 >.
) ) )
260259expimpd 586 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  r  e.  ( 0 [,] 1
) )  /\  (
u  e.  II  /\  v  e.  II )
)  ->  ( (
( r  e.  u  /\  0  e.  v
)  /\  ( E. w  e.  v  ( K  |`  ( u  X.  { w } ) )  e.  ( ( ( II  tX  II )t  ( u  X.  { w } ) )  Cn  C )  ->  ( K  |`  ( u  X.  v ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  v ) )  Cn  C ) ) )  ->  K  e.  ( ( ( II 
tX  II )  CnP 
C ) `  <. r ,  0 >. )
) )
261184, 260syl5bi 208 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  r  e.  ( 0 [,] 1
) )  /\  (
u  e.  II  /\  v  e.  II )
)  ->  ( (
r  e.  u  /\  0  e.  v  /\  ( E. w  e.  v  ( K  |`  (
u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) )  ->  K  e.  ( ( ( II  tX  II )  CnP  C ) `
 <. r ,  0
>. ) ) )
262261rexlimdvva 2687 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  ( E. u  e.  II  E. v  e.  II  ( r  e.  u  /\  0  e.  v  /\  ( E. w  e.  v  ( K  |`  ( u  X.  { w } ) )  e.  ( ( ( II 
tX  II )t  ( u  X.  { w }
) )  Cn  C
)  ->  ( K  |`  ( u  X.  v
) )  e.  ( ( ( II  tX  II )t  ( u  X.  v ) )  Cn  C ) ) )  ->  K  e.  ( ( ( II  tX  II )  CnP  C ) `
 <. r ,  0
>. ) ) )
263183, 262mpd 14 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  K  e.  ( ( ( II 
tX  II )  CnP 
C ) `  <. r ,  0 >. )
)
264 fveq2 5541 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  <. r ,  0
>.  ->  ( ( ( II  tX  II )  CnP  C ) `  z
)  =  ( ( ( II  tX  II )  CnP  C ) `  <. r ,  0 >.
) )
265264eleq2d 2363 . . . . . . . . . . . . . . . . 17  |-  ( z  =  <. r ,  0
>.  ->  ( K  e.  ( ( ( II 
tX  II )  CnP 
C ) `  z
)  <->  K  e.  (
( ( II  tX  II )  CnP  C ) `
 <. r ,  0
>. ) ) )
266265, 69elrab2 2938 . . . . . . . . . . . . . . . 16  |-  ( <.
r ,  0 >.  e.  M  <->  ( <. r ,  0 >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) )  /\  K  e.  ( ( ( II  tX  II )  CnP  C ) `
 <. r ,  0
>. ) ) )
267176, 263, 266sylanbrc 645 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  <. r ,  0 >.  e.  M
)
268 elsni 3677 . . . . . . . . . . . . . . . . 17  |-  ( a  e.  { 0 }  ->  a  =  0 )
269268opeq2d 3819 . . . . . . . . . . . . . . . 16  |-  ( a  e.  { 0 }  ->  <. r ,  a
>.  =  <. r ,  0 >. )
270269eleq1d 2362 . . . . . . . . . . . . . . 15  |-  ( a  e.  { 0 }  ->  ( <. r ,  a >.  e.  M  <->  <.
r ,  0 >.  e.  M ) )
271267, 270syl5ibrcom 213 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  (
a  e.  { 0 }  ->  <. r ,  a >.  e.  M
) )
272271expimpd 586 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( r  e.  ( 0 [,] 1
)  /\  a  e.  { 0 } )  ->  <. r ,  a >.  e.  M ) )
273173, 272syl5bi 208 . . . . . . . . . . . 12  |-  ( ph  ->  ( <. r ,  a
>.