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

Theorem cvmlift2lem12 24773
Description: Lemma for cvmlift2 24775. (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 24766 . 2  |-  ( ph  ->  K : ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) ) --> B )
9 iunid 4080 . . . . . . 7  |-  U_ a  e.  ( 0 [,] 1
) { a }  =  ( 0 [,] 1 )
109xpeq2i 4832 . . . . . 6  |-  ( ( 0 [,] 1 )  X.  U_ a  e.  ( 0 [,] 1
) { a } )  =  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )
11 xpiundi 4865 . . . . . 6  |-  ( ( 0 [,] 1 )  X.  U_ a  e.  ( 0 [,] 1
) { a } )  =  U_ a  e.  ( 0 [,] 1
) ( ( 0 [,] 1 )  X. 
{ a } )
1210, 11eqtr3i 2402 . . . . 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 18775 . . . . . . . . 9  |-  ( 0 [,] 1 )  = 
U. II
15 iicon 18781 . . . . . . . . . 10  |-  II  e.  Con
1615a1i 11 . . . . . . . . 9  |-  ( ph  ->  II  e.  Con )
17 inss1 3497 . . . . . . . . . 10  |-  ( II 
i^i  ( Clsd `  II ) )  C_  II
18 iicmp 18780 . . . . . . . . . . . . . . 15  |-  II  e.  Comp
1918a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  II  e.  Comp )
20 iitop 18774 . . . . . . . . . . . . . . 15  |-  II  e.  Top
2120a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  II  e.  Top )
2220, 20txtopi 17536 . . . . . . . . . . . . . . . 16  |-  ( II 
tX  II )  e. 
Top
2314neiss2 17081 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( II  e.  Top  /\  u  e.  ( ( nei `  II ) `  { r } ) )  ->  { r }  C_  ( 0 [,] 1 ) )
2420, 23mpan 652 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  e.  ( ( nei `  II ) `  {
r } )  ->  { r }  C_  ( 0 [,] 1
) )
25 vex 2895 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  r  e. 
_V
2625snss 3862 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( r  e.  ( 0 [,] 1 )  <->  { r }  C_  ( 0 [,] 1 ) )
2724, 26sylibr 204 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  e.  ( ( nei `  II ) `  {
r } )  -> 
r  e.  ( 0 [,] 1 ) )
2827a1d 23 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  e.  ( ( nei `  II ) `  {
r } )  -> 
( ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M )  -> 
r  e.  ( 0 [,] 1 ) ) )
2928rexlimiv 2760 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. u  e.  ( ( nei `  II ) `
 { r } ) ( ( u  X.  { a } )  C_  M  <->  ( u  X.  { t } ) 
C_  M )  -> 
r  e.  ( 0 [,] 1 ) )
3029adantl 453 . . . . . . . . . . . . . . . . . . 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 444 . . . . . . . . . . . . . . . . . . 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 519 . . . . . . . . . . . . . . . . . 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 4416 . . . . . . . . . . . . . . . . 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 4817 . . . . . . . . . . . . . . . . 17  |-  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )  =  { <. r ,  t
>.  |  ( r  e.  ( 0 [,] 1
)  /\  t  e.  ( 0 [,] 1
) ) }
3633, 34, 353sstr4i 3323 . . . . . . . . . . . . . . . 16  |-  S  C_  ( ( 0 [,] 1 )  X.  (
0 [,] 1 ) )
3720, 20, 14, 14txunii 17539 . . . . . . . . . . . . . . . . 17  |-  ( ( 0 [,] 1 )  X.  ( 0 [,] 1 ) )  = 
U. ( II  tX  II )
3837ntropn 17029 . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . 15  |-  ( ( int `  ( II 
tX  II ) ) `
 S )  e.  ( II  tX  II )
4039a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  (
( int `  (
II  tX  II )
) `  S )  e.  ( II  tX  II ) )
412adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  F  e.  ( C CovMap  J ) )
423adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  G  e.  ( (
II  tX  II )  Cn  J ) )
434adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  P  e.  B )
445adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  -> 
( F `  P
)  =  ( 0 G 0 ) )
45 eqid 2380 . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  -> 
b  e.  ( 0 [,] 1 ) )
47 simprl 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  -> 
a  e.  ( 0 [,] 1 ) )
481, 41, 42, 43, 44, 6, 7, 45, 46, 47cvmlift2lem10 24771 . . . . . . . . . . . . . . . . . . 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 11 . . . . . . . . . . . . . . . . . . . . . . 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 11 . . . . . . . . . . . . . . . . . . . . . . 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 11 . . . . . . . . . . . . . . . . . . . . . . . 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 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 ) ) ) )  ->  u  e.  II )
53 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . 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 17548 . . . . . . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( r  e.  u  /\  t  e.  v )  ->  t  e.  v )
57 elunii 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( t  e.  v  /\  v  e.  II )  ->  t  e.  U. II )
5857, 14syl6eleqr 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( t  e.  v  /\  v  e.  II )  ->  t  e.  ( 0 [,] 1 ) )
5956, 53, 58syl2anr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( II  e.  Top  /\  u  e.  II  /\  r  e.  u )  ->  u  e.  ( ( nei `  II ) `
 { r } ) )
6460, 61, 62, 63syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  w  ->  { c }  =  { w } )
7473xpeq2d 4835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  w  ->  (
u  X.  { c } )  =  ( u  X.  { w } ) )
7574reseq2d 5079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( c  =  w  ->  ( K  |`  ( u  X.  { c } ) )  =  ( K  |`  ( u  X.  {
w } ) ) )
7674oveq2d 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  w  ->  (
( II  tX  II )t  ( u  X.  { c } ) )  =  ( ( II  tX  II )t  ( u  X.  { w } ) ) )
7776oveq1d 6028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( c  =  w  ->  (
( ( II  tX  II )t  ( u  X.  { c } ) )  Cn  C )  =  ( ( ( II  tX  II )t  (
u  X.  { w } ) )  Cn  C ) )
7875, 77eleq12d 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 24772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 24772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2703 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 519 . . . . . . . . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . . . . . . . . . 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 1639 . . . . . . . . . . . . . . . . . . . . . . . 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 4817 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( u  X.  v )  =  { <. r ,  t
>.  |  ( r  e.  u  /\  t  e.  v ) }
9190, 34sseq12i 3310 . . . . . . . . . . . . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . . . . . . . . . . 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 204 . . . . . . . . . . . . . . . . . . . . . . 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 17038 . . . . . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . . . . . 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 963 . . . . . . . . . . . . . . . . . . . . . . 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 964 . . . . . . . . . . . . . . . . . . . . . . 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 4843 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  e.  u  /\  a  e.  v )  -> 
<. b ,  a >.  e.  ( u  X.  v
) )
10097, 98, 99syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 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 3285 . . . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  <. b ,  a >.  e.  ( ( int `  (
II  tX  II )
) `  S )
)
105 vex 2895 . . . . . . . . . . . . . . . . . . 19  |-  a  e. 
_V
106 opeq2 3920 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  a  ->  <. b ,  w >.  =  <. b ,  a >. )
107106eleq1d 2446 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  a  ->  ( <. b ,  w >.  e.  ( ( int `  (
II  tX  II )
) `  S )  <->  <.
b ,  a >.  e.  ( ( int `  (
II  tX  II )
) `  S )
) )
108105, 107ralsn 3785 . . . . . . . . . . . . . . . . . 18  |-  ( A. w  e.  { a } <. b ,  w >.  e.  ( ( int `  ( II  tX  II ) ) `  S
)  <->  <. b ,  a
>.  e.  ( ( int `  ( II  tX  II ) ) `  S
) )
109104, 108sylibr 204 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  ( 0 [,] 1
)  /\  b  e.  ( 0 [,] 1
) ) )  ->  A. w  e.  { a } <. b ,  w >.  e.  ( ( int `  ( II  tX  II ) ) `  S
) )
110109anassrs 630 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  a  e.  ( 0 [,] 1
) )  /\  b  e.  ( 0 [,] 1
) )  ->  A. w  e.  { a } <. b ,  w >.  e.  ( ( int `  (
II  tX  II )
) `  S )
)
111110ralrimiva 2725 . . . . . . . . . . . . . . 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 3274 . . . . . . . . . . . . . . . 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 2440 . . . . . . . . . . . . . . . . 17  |-  ( u  =  <. b ,  w >.  ->  ( u  e.  ( ( int `  (
II  tX  II )
) `  S )  <->  <.
b ,  w >.  e.  ( ( int `  (
II  tX  II )
) `  S )
) )
114113ralxp 4949 . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . 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 204 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  (
( 0 [,] 1
)  X.  { a } )  C_  (
( int `  (
II  tX  II )
) `  S )
)
117 simpr 448 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  a  e.  ( 0 [,] 1
) )
11814, 14, 19, 21, 40, 116, 117txtube 17586 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  E. v  e.  II  ( a  e.  v  /\  ( ( 0 [,] 1 )  X.  v )  C_  ( ( int `  (
II  tX  II )
) `  S )
) )
11937ntrss2 17037 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( II  tX  II )  e.  Top  /\  S  C_  ( ( 0 [,] 1 )  X.  (
0 [,] 1 ) ) )  ->  (
( int `  (
II  tX  II )
) `  S )  C_  S )
12022, 36, 119mp2an 654 . . . . . . . . . . . . . . . . . 18  |-  ( ( int `  ( II 
tX  II ) ) `
 S )  C_  S
121 sstr 3292 . . . . . . . . . . . . . . . . . 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 653 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 0 [,] 1
)  X.  v ) 
C_  ( ( int `  ( II  tX  II ) ) `  S
)  ->  ( (
0 [,] 1 )  X.  v )  C_  S )
123 df-xp 4817 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0 [,] 1 )  X.  v )  =  { <. r ,  t
>.  |  ( r  e.  ( 0 [,] 1
)  /\  t  e.  v ) }
124123, 34sseq12i 3310 . . . . . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . . . . . . . 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 2679 . . . . . . . . . . . . . . . . . . 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 2804 . . . . . . . . . . . . . . . . . . 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 265 . . . . . . . . . . . . . . . . . 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 241 . . . . . . . . . . . . . . . . 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 189 . . . . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . . . . 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 2717 . . . . . . . . . . . . . . . . . . 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 24761 . . . . . . . . . . . . . . . . . . . 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 192 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( u  X.  {
a } )  C_  M 
<->  ( u  X.  {
t } )  C_  M )  <->  ( (
u  X.  { t } )  C_  M  <->  ( u  X.  { a } )  C_  M
) )
135134rexbii 2667 . . . . . . . . . . . . . . . . . . . . . 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 2666 . . . . . . . . . . . . . . . . . . . . 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 24761 . . . . . . . . . . . . . . . . . . . . 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 188 . . . . . . . . . . . . . . . . . . . 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 184 . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . 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 )
)
14113rabeq2i 2889 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  A  <->  ( a  e.  ( 0 [,] 1
)  /\  ( (
0 [,] 1 )  X.  { a } )  C_  M )
)
142141baib 872 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  ( 0 [,] 1 )  ->  (
a  e.  A  <->  ( (
0 [,] 1 )  X.  { a } )  C_  M )
)
143142ad3antlr 712 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  a  e.  ( 0 [,] 1 ) )  /\  v  e.  II )  /\  t  e.  v )  ->  ( a  e.  A  <->  ( ( 0 [,] 1 )  X. 
{ a } ) 
C_  M ) )
144 elssuni 3978 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  e.  II  ->  v  C_ 
U. II )
145144, 14syl6sseqr 3331 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  II  ->  v  C_  ( 0 [,] 1
) )
146145adantl 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  a  e.  ( 0 [,] 1
) )  /\  v  e.  II )  ->  v  C_  ( 0 [,] 1
) )
147146sselda 3284 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  a  e.  ( 0 [,] 1 ) )  /\  v  e.  II )  /\  t  e.  v )  ->  t  e.  ( 0 [,] 1
) )
148 sneq 3761 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  t  ->  { a }  =  { t } )
149148xpeq2d 4835 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  t  ->  (
( 0 [,] 1
)  X.  { a } )  =  ( ( 0 [,] 1
)  X.  { t } ) )
150149sseq1d 3311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  t  ->  (
( ( 0 [,] 1 )  X.  {
a } )  C_  M 
<->  ( ( 0 [,] 1 )  X.  {
t } )  C_  M ) )
151150, 13elrab2 3030 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  e.  A  <->  ( t  e.  ( 0 [,] 1
)  /\  ( (
0 [,] 1 )  X.  { t } )  C_  M )
)
152151baib 872 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  e.  ( 0 [,] 1 )  ->  (
t  e.  A  <->  ( (
0 [,] 1 )  X.  { t } )  C_  M )
)
153147, 152syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  a  e.  ( 0 [,] 1 ) )  /\  v  e.  II )  /\  t  e.  v )  ->  ( t  e.  A  <->  ( ( 0 [,] 1 )  X. 
{ t } ) 
C_  M ) )
154143, 153bibi12d 313 . . . . . . . . . . . . . . . . . 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
) ) )
155140, 154syl5ibr 213 . . . . . . . . . . . . . . . . 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
) ) )
156155ralimdva 2720 . . . . . . . . . . . . . . . 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
) ) )
157130, 156syl5 30 . . . . . . . . . . . . . . 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
) ) )
158157anim2d 549 . . . . . . . . . . . . . 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
) ) ) )
159158reximdva 2754 . . . . . . . . . . . . 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
) ) ) )
160118, 159mpd 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( 0 [,] 1
) )  ->  E. v  e.  II  ( a  e.  v  /\  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) )
161160ralrimiva 2725 . . . . . . . . . . 11  |-  ( ph  ->  A. a  e.  ( 0 [,] 1 ) E. v  e.  II  ( a  e.  v  /\  A. t  e.  v  ( a  e.  A  <->  t  e.  A
) ) )
162 ssrab2 3364 . . . . . . . . . . . . 13  |-  { a  e.  ( 0 [,] 1 )  |  ( ( 0 [,] 1
)  X.  { a } )  C_  M }  C_  ( 0 [,] 1 )
16313, 162eqsstri 3314 . . . . . . . . . . . 12  |-  A  C_  ( 0 [,] 1
)
16414isclo 17067 . . . . . . . . . . . 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
) ) ) )
16520, 163, 164mp2an 654 . . . . . . . . . . 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
) ) )
166161, 165sylibr 204 . . . . . . . . . 10  |-  ( ph  ->  A  e.  ( II 
i^i  ( Clsd `  II ) ) )
16717, 166sseldi 3282 . . . . . . . . 9  |-  ( ph  ->  A  e.  II )
168 0elunit 10940 . . . . . . . . . . . 12  |-  0  e.  ( 0 [,] 1
)
169168a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( 0 [,] 1 ) )
170 relxp 4916 . . . . . . . . . . . . 13  |-  Rel  (
( 0 [,] 1
)  X.  { 0 } )
171170a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  Rel  ( ( 0 [,] 1 )  X. 
{ 0 } ) )
172 opelxp 4841 . . . . . . . . . . . . 13  |-  ( <.
r ,  a >.  e.  ( ( 0 [,] 1 )  X.  {
0 } )  <->  ( r  e.  ( 0 [,] 1
)  /\  a  e.  { 0 } ) )
173 id 20 . . . . . . . . . . . . . . . . 17  |-  ( r  e.  ( 0 [,] 1 )  ->  r  e.  ( 0 [,] 1
) )
174 opelxpi 4843 . . . . . . . . . . . . . . . . 17  |-  ( ( r  e.  ( 0 [,] 1 )  /\  0  e.  ( 0 [,] 1 ) )  ->  <. r ,  0
>.  e.  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) )
175173, 169, 174syl2anr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  <. r ,  0 >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) ) )
1762adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  F  e.  ( C CovMap  J ) )
1773adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  G  e.  ( ( II  tX  II )  Cn  J
) )
1784adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  P  e.  B )
1795adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  ( F `  P )  =  ( 0 G 0 ) )
180 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  r  e.  ( 0 [,] 1
) )
181168a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  0  e.  ( 0 [,] 1
) )
1821, 176, 177, 178, 179, 6, 7, 45, 180, 181cvmlift2lem10 24771 . . . . . . . . . . . . . . . . 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 ) ) ) )
183 df-3an 938 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
184 simprr 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  0  e.  v )
1858ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
186 ffn 5524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( K : ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) ) --> B  ->  K  Fn  ( (
0 [,] 1 )  X.  ( 0 [,] 1 ) ) )
187185, 186syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
188 fnov 6110 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( K  Fn  ( ( 0 [,] 1 )  X.  ( 0 [,] 1
) )  <->  K  =  ( b  e.  ( 0 [,] 1 ) ,  w  e.  ( 0 [,] 1 ) 
|->  ( b K w ) ) )
189187, 188sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
190189reseq1d 5078 . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
191 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  u  e.  II )
192 elssuni 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( u  e.  II  ->  u  C_ 
U. II )
193192, 14syl6sseqr 3331 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( u  e.  II  ->  u  C_  ( 0 [,] 1
) )
194191, 193syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  u  C_  ( 0 [,] 1
) )
195169snssd 3879 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  { 0 }  C_  ( 0 [,] 1
) )
196195ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  { 0 }  C_  ( 0 [,] 1 ) )
197 resmpt2 6100 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
198194, 196, 197syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
199194sselda 3284 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
200 simplll 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  ph )
2011, 2, 3, 4, 5, 6, 7cvmlift2lem8 24769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  b  e.  ( 0 [,] 1
) )  ->  (
b K 0 )  =  ( H `  b ) )
202200, 201sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
203199, 202syldan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
204 elsni 3774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  { 0 }  ->  w  =  0 )
205204oveq2d 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  e.  { 0 }  ->  ( b K w )  =  ( b K 0 ) )
206205eqeq1d 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  { 0 }  ->  ( ( b K w )  =  ( H `  b
)  <->  ( b K 0 )  =  ( H `  b ) ) )
207203, 206syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
2082073impia 1150 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
209208mpt2eq3dva 6070 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
210190, 198, 2093eqtrd 2416 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
211 eqid 2380 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( IIt  u )  =  ( IIt  u )
212 iitopon 18773 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  II  e.  (TopOn `  ( 0 [,] 1 ) )
213212a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  II  e.  (TopOn `  ( 0 [,] 1 ) ) )
214 eqid 2380 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( IIt  {
0 } )  =  ( IIt  { 0 } )
215213, 213cnmpt1st 17614 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
2161, 2, 3, 4, 5, 6cvmlift2lem2 24763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( H  e.  ( II  Cn  C )  /\  ( F  o.  H )  =  ( z  e.  ( 0 [,] 1 )  |->  ( z G 0 ) )  /\  ( H `
 0 )  =  P ) )
217216simp1d 969 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  H  e.  ( II 
Cn  C ) )
218200, 217syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  H  e.  ( II  Cn  C
) )
219213, 213, 215, 218cnmpt21f 17618 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
220211, 213, 194, 214, 213, 196, 219cnmpt2res 17623 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
221 vex 2895 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  u  e. 
_V
222 snex 4339 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  { 0 }  e.  _V
223 txrest 17577 . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) )
22420, 20, 221, 222, 223mp4an 655 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( II  tX  II )t  (
u  X.  { 0 } ) )  =  ( ( IIt  u ) 
tX  ( IIt  { 0 } ) )
225224oveq1i 6023 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( II  tX  II )t  ( u  X.  { 0 } ) )  Cn  C )  =  ( ( ( IIt  u ) 
tX  ( IIt  { 0 } ) )  Cn  C )
226220, 225syl6eleqr 2471 . . . . . . . . . . . . . . . . . . . . . . 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
) )
227210, 226eqeltrd 2454 . . . . . . . . . . . . . . . . . . . . . 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 ) )
228 sneq 3761 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  0  ->  { w }  =  { 0 } )
229228xpeq2d 4835 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  0  ->  (
u  X.  { w } )  =  ( u  X.  { 0 } ) )
230229reseq2d 5079 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  0  ->  ( K  |`  ( u  X.  { w } ) )  =  ( K  |`  ( u  X.  {
0 } ) ) )
231229oveq2d 6029 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  0  ->  (
( II  tX  II )t  ( u  X.  { w } ) )  =  ( ( II  tX  II )t  ( u  X.  { 0 } ) ) )
232231oveq1d 6028 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  0  ->  (
( ( II  tX  II )t  ( u  X.  { w } ) )  Cn  C )  =  ( ( ( II  tX  II )t  (
u  X.  { 0 } ) )  Cn  C ) )
233230, 232eleq12d 2448 . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
234233rspcev 2988 . . . . . . . . . . . . . . . . . . . . . 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 ) )
235184, 227, 234syl2anc 643 . . . . . . . . . . . . . . . . . . . . 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 ) )
236 opelxpi 4843 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( r  e.  u  /\  0  e.  v )  -> 
<. r ,  0 >.  e.  ( u  X.  v
) )
237236adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  <. r ,  0 >.  e.  ( u  X.  v ) )
238 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  v  e.  II )
239238, 145syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  v  C_  ( 0 [,] 1
) )
240 xpss12 4914 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( u  C_  ( 0 [,] 1 )  /\  v  C_  ( 0 [,] 1 ) )  -> 
( u  X.  v
)  C_  ( (
0 [,] 1 )  X.  ( 0 [,] 1 ) ) )
241194, 239, 240syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
24237restuni 17141 . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
24322, 241, 242sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
244237, 243eleqtrd 2456 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
245 eqid 2380 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  U. (
( II  tX  II )t  ( u  X.  v
) )  =  U. ( ( II  tX  II )t  ( u  X.  v ) )
246245cncnpi 17257 . . . . . . . . . . . . . . . . . . . . . . . 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 >. )
)
247246expcom 425 . . . . . . . . . . . . . . . . . . . . . . 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
>. ) ) )
248244, 247syl 16 . . . . . . . . . . . . . . . . . . . . . 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 >.
) ) )
24922a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  (
II  tX  II )  e.  Top )
25020a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  r  e.  ( 0 [,] 1 ) )  /\  ( u  e.  II  /\  v  e.  II ) )  /\  ( r  e.  u  /\  0  e.  v
) )  ->  II  e.  Top )
251250, 250, 191, 238, 54syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
252 isopn3i 17062 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( II  tX  II )  e.  Top  /\  (
u  X.  v )  e.  ( II  tX  II ) )  ->  (
( int `  (
II  tX  II )
) `  ( u  X.  v ) )  =  ( u  X.  v
) )
25322, 251, 252sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . 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
) )
254237, 253eleqtrrd 2457 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
25537, 1cnprest 17268 . . . . . . . . . . . . . . . . . . . . . . 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
>. ) ) )
256249, 241, 254, 185, 255syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . 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 >.
) ) )
257248, 256sylibrd 226 . . . . . . . . . . . . . . . . . . . . 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 >. )
) )
258235, 257embantd 52 . . . . . . . . . . . . . . . . . . . 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 >.
) ) )
259258expimpd 587 . . . . . . . . . . . . . . . . . . 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 >. )
) )
260183, 259syl5bi 209 . . . . . . . . . . . . . . . . . 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
>. ) ) )
261260rexlimdvva 2773 . . . . . . . . . . . . . . . . 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
>. ) ) )
262182, 261mpd 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  K  e.  ( ( ( II 
tX  II )  CnP 
C ) `  <. r ,  0 >. )
)
263 fveq2 5661 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  <. r ,  0
>.  ->  ( ( ( II  tX  II )  CnP  C ) `  z
)  =  ( ( ( II  tX  II )  CnP  C ) `  <. r ,  0 >.
) )
264263eleq2d 2447 . . . . . . . . . . . . . . . . 17  |-  ( z  =  <. r ,  0
>.  ->  ( K  e.  ( ( ( II 
tX  II )  CnP 
C ) `  z
)  <->  K  e.  (
( ( II  tX  II )  CnP  C ) `
 <. r ,  0
>. ) ) )
265264, 69elrab2 3030 . . . . . . . . . . . . . . . 16  |-  ( <.
r ,  0 >.  e.  M  <->  ( <. r ,  0 >.  e.  ( ( 0 [,] 1
)  X.  ( 0 [,] 1 ) )  /\  K  e.  ( ( ( II  tX  II )  CnP  C ) `
 <. r ,  0
>. ) ) )
266175, 262, 265sylanbrc 646 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  <. r ,  0 >.  e.  M
)
267 elsni 3774 . . . . . . . . . . . . . . . . 17  |-  ( a  e.  { 0 }  ->  a  =  0 )
268267opeq2d 3926 . . . . . . . . . . . . . . . 16  |-  ( a  e.  { 0 }  ->  <. r ,  a
>.  =  <. r ,  0 >. )
269268eleq1d 2446 . . . . . . . . . . . . . . 15  |-  ( a  e.  { 0 }  ->  ( <. r ,  a >.  e.  M  <->  <.
r ,  0 >.  e.  M ) )
270266, 269syl5ibrcom 214 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  r  e.  ( 0 [,] 1
) )  ->  (
a  e.  { 0 }  ->  <. r ,  a >.  e.  M
) )
271270expimpd 587 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( r  e.  ( 0 [,] 1
)  /\  a  e.  { 0 } )  ->  <. r ,  a >.  e.  M ) )
272172, 271syl5bi 209 . . . . . . . . . . . 12  |-  ( ph  ->  ( <. r ,  a
>.  e.  ( ( 0 [,] 1 )  X. 
{ 0 } )  ->  <. r ,  a
>.  e.  M ) )
273171, 272relssdv 4901 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 0 [,] 1 )  X.  {
0 } )  C_  M )
274 sneq 3761 . . . . . . . . . . . . . 14  |-  ( a  =  0  ->  { a }  =  { 0 } )
275274xpeq2d 4835 . . . . . . . . . . . . 13  |-  ( a  =  0  ->  (
( 0 [,] 1
)  X.  { a } )  =  ( ( 0 [,] 1
)  X.  { 0 } ) )
276275sseq1d 3311 . . . . . . . . . . . 12  |-  ( a  =  0  ->  (
( ( 0 [,] 1 )  X.  {
a } )  C_  M 
<->  ( ( 0 [,] 1 )