Metamath Proof Explorer

Theorem cvmlift2lem12

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-2015)

Ref Expression
Hypotheses 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 cvmlift2lem12 
|- ( ph -> K e. ( ( II tX II ) Cn C ) )

Proof

Step Hyp Ref Expression
1 cvmlift2.b 
 |-  B = U. C
2 cvmlift2.f 
 |-  ( ph -> F e. ( C CovMap J ) )
3 cvmlift2.g 
 |-  ( ph -> G e. ( ( II tX II ) Cn J ) )
4 cvmlift2.p 
 |-  ( ph -> P e. B )
5 cvmlift2.i 
 |-  ( ph -> ( F ` P ) = ( 0 G 0 ) )
6 cvmlift2.h 
 |-  H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( f ` 0 ) = P ) )
7 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 ) )
8 cvmlift2.m 
 |-  M = { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) }
9 cvmlift2.a 
 |-  A = { a e. ( 0 [,] 1 ) | ( ( 0 [,] 1 ) X. { a } ) C_ M }
10 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 ) ) }
11 1 2 3 4 5 6 7 cvmlift2lem5 
 |-  ( ph -> K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B )
12 iunid 
 |-  U_ a e. ( 0 [,] 1 ) { a } = ( 0 [,] 1 )
13 12 xpeq2i 
 |-  ( ( 0 [,] 1 ) X. U_ a e. ( 0 [,] 1 ) { a } ) = ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) )
14 xpiundi 
 |-  ( ( 0 [,] 1 ) X. U_ a e. ( 0 [,] 1 ) { a } ) = U_ a e. ( 0 [,] 1 ) ( ( 0 [,] 1 ) X. { a } )
15 13 14 eqtr3i 
 |-  ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) = U_ a e. ( 0 [,] 1 ) ( ( 0 [,] 1 ) X. { a } )
16 iiuni 
 |-  ( 0 [,] 1 ) = U. II
17 iiconn 
 |-  II e. Conn
18 17 a1i 
 |-  ( ph -> II e. Conn )
19 inss1 
 |-  ( II i^i ( Clsd ` II ) ) C_ II
20 iicmp 
 |-  II e. Comp
21 20 a1i 
 |-  ( ( ph /\ a e. ( 0 [,] 1 ) ) -> II e. Comp )
22 iitop 
 |-  II e. Top
23 22 a1i 
 |-  ( ( ph /\ a e. ( 0 [,] 1 ) ) -> II e. Top )
24 22 22 txtopi 
 |-  ( II tX II ) e. Top
25 16 neiss2 
 |-  ( ( II e. Top /\ u e. ( ( nei ` II ) ` { r } ) ) -> { r } C_ ( 0 [,] 1 ) )
26 22 25 mpan 
 |-  ( u e. ( ( nei ` II ) ` { r } ) -> { r } C_ ( 0 [,] 1 ) )
27 vex 
 |-  r e. _V
28 27 snss 
 |-  ( r e. ( 0 [,] 1 ) <-> { r } C_ ( 0 [,] 1 ) )
29 26 28 sylibr 
 |-  ( u e. ( ( nei ` II ) ` { r } ) -> r e. ( 0 [,] 1 ) )
30 29 a1d 
 |-  ( u e. ( ( nei ` II ) ` { r } ) -> ( ( ( u X. { a } ) C_ M <-> ( u X. { t } ) C_ M ) -> r e. ( 0 [,] 1 ) ) )
31 30 rexlimiv 
 |-  ( E. u e. ( ( nei ` II ) ` { r } ) ( ( u X. { a } ) C_ M <-> ( u X. { t } ) C_ M ) -> r e. ( 0 [,] 1 ) )
32 31 adantl 
 |-  ( ( t e. ( 0 [,] 1 ) /\ E. u e. ( ( nei ` II ) ` { r } ) ( ( u X. { a } ) C_ M <-> ( u X. { t } ) C_ M ) ) -> r e. ( 0 [,] 1 ) )
33 simpl 
 |-  ( ( t e. ( 0 [,] 1 ) /\ E. u e. ( ( nei ` II ) ` { r } ) ( ( u X. { a } ) C_ M <-> ( u X. { t } ) C_ M ) ) -> t e. ( 0 [,] 1 ) )
34 32 33 jca 
 |-  ( ( 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 ) ) )
35 34 ssopab2i 
 |-  { <. 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 ) ) }
36 df-xp 
 |-  ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) = { <. r , t >. | ( r e. ( 0 [,] 1 ) /\ t e. ( 0 [,] 1 ) ) }
37 35 10 36 3sstr4i 
 |-  S C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) )
38 22 22 16 16 txunii 
 |-  ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) = U. ( II tX II )
39 38 ntropn 
 |-  ( ( ( II tX II ) e. Top /\ S C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( ( int ` ( II tX II ) ) ` S ) e. ( II tX II ) )
40 24 37 39 mp2an 
 |-  ( ( int ` ( II tX II ) ) ` S ) e. ( II tX II )
41 40 a1i 
 |-  ( ( ph /\ a e. ( 0 [,] 1 ) ) -> ( ( int ` ( II tX II ) ) ` S ) e. ( II tX II ) )
42 2 adantr 
 |-  ( ( ph /\ ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) ) -> F e. ( C CovMap J ) )
43 3 adantr 
 |-  ( ( ph /\ ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) ) -> G e. ( ( II tX II ) Cn J ) )
44 4 adantr 
 |-  ( ( ph /\ ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) ) -> P e. B )
45 5 adantr 
 |-  ( ( ph /\ ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) ) -> ( F ` P ) = ( 0 G 0 ) )
46 eqid 
 |-  ( 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. ( ( C |`t c ) Homeo ( J |`t 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. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) } )
47 simprr 
 |-  ( ( ph /\ ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) ) -> b e. ( 0 [,] 1 ) )
48 simprl 
 |-  ( ( ph /\ ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) ) -> a e. ( 0 [,] 1 ) )
49 1 42 43 44 45 6 7 46 47 48 cvmlift2lem10 
 |-  ( ( 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 ) ) ) )
50 24 a1i 
 |-  ( ( ( ( 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 )
51 37 a1i 
 |-  ( ( ( ( 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 ) ) )
52 22 a1i 
 |-  ( ( ( ( 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 )
53 simplrl 
 |-  ( ( ( ( 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 )
54 simplrr 
 |-  ( ( ( ( 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 )
55 txopn 
 |-  ( ( ( II e. Top /\ II e. Top ) /\ ( u e. II /\ v e. II ) ) -> ( u X. v ) e. ( II tX II ) )
56 52 52 53 54 55 syl22anc 
 |-  ( ( ( ( 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 ) )
57 simpr 
 |-  ( ( r e. u /\ t e. v ) -> t e. v )
58 elunii 
 |-  ( ( t e. v /\ v e. II ) -> t e. U. II )
59 58 16 eleqtrrdi 
 |-  ( ( t e. v /\ v e. II ) -> t e. ( 0 [,] 1 ) )
60 57 54 59 syl2anr 
 |-  ( ( ( ( ( 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 ) )
61 22 a1i 
 |-  ( ( ( ( ( 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 )
62 53 adantr 
 |-  ( ( ( ( ( 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 )
63 simprl 
 |-  ( ( ( ( ( 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 )
64 opnneip 
 |-  ( ( II e. Top /\ u e. II /\ r e. u ) -> u e. ( ( nei ` II ) ` { r } ) )
65 61 62 63 64 syl3anc 
 |-  ( ( ( ( ( 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 } ) )
66 42 ad3antrrr 
 |-  ( ( ( ( ( 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 ) )
67 43 ad3antrrr 
 |-  ( ( ( ( ( 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 ) )
68 44 ad3antrrr 
 |-  ( ( ( ( ( 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 )
69 45 ad3antrrr 
 |-  ( ( ( ( ( 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 ) )
70 54 adantr 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( c = w -> { c } = { w } )
74 73 xpeq2d 
 |-  ( c = w -> ( u X. { c } ) = ( u X. { w } ) )
75 74 reseq2d 
 |-  ( c = w -> ( K |` ( u X. { c } ) ) = ( K |` ( u X. { w } ) ) )
76 74 oveq2d 
 |-  ( c = w -> ( ( II tX II ) |`t ( u X. { c } ) ) = ( ( II tX II ) |`t ( u X. { w } ) ) )
77 76 oveq1d 
 |-  ( c = w -> ( ( ( II tX II ) |`t ( u X. { c } ) ) Cn C ) = ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) )
78 75 77 eleq12d 
 |-  ( 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 ) ) )
79 78 cbvrexvw 
 |-  ( 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 
 |-  ( ( ( ( ( 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 ) ) )
81 79 80 biimtrid 
 |-  ( ( ( ( ( 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 ) ) )
82 1 66 67 68 69 6 7 8 62 70 71 72 81 cvmlift2lem11 
 |-  ( ( ( ( ( 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 ) )
83 1 66 67 68 69 6 7 8 62 70 72 71 81 cvmlift2lem11 
 |-  ( ( ( ( ( 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 ) )
84 82 83 impbid 
 |-  ( ( ( ( ( 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 
 |-  ( ( 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 ) )
86 65 84 85 syl2anc 
 |-  ( ( ( ( ( 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 ) )
87 60 86 jca 
 |-  ( ( ( ( ( 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 ) ) )
88 87 ex 
 |-  ( ( ( ( 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 ) ) ) )
89 88 alrimivv 
 |-  ( ( ( ( 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 
 |-  ( u X. v ) = { <. r , t >. | ( r e. u /\ t e. v ) }
91 90 10 sseq12i 
 |-  ( ( 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 ssopab2bw 
 |-  ( { <. 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 ) ) ) )
93 91 92 bitri 
 |-  ( ( 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 ) ) ) )
94 89 93 sylibr 
 |-  ( ( ( ( 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 )
95 38 ssntr 
 |-  ( ( ( ( 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 ) )
96 50 51 56 94 95 syl22anc 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( b e. u /\ a e. v ) -> <. b , a >. e. ( u X. v ) )
100 97 98 99 syl2anc 
 |-  ( ( ( ( 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 ) )
101 96 100 sseldd 
 |-  ( ( ( ( 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 ) )
102 101 ex 
 |-  ( ( ( 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 ) ) )
103 102 rexlimdvva 
 |-  ( ( 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 ) ) )
104 49 103 mpd 
 |-  ( ( ph /\ ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) ) -> <. b , a >. e. ( ( int ` ( II tX II ) ) ` S ) )
105 vex 
 |-  a e. _V
106 opeq2 
 |-  ( w = a -> <. b , w >. = <. b , a >. )
107 106 eleq1d 
 |-  ( w = a -> ( <. b , w >. e. ( ( int ` ( II tX II ) ) ` S ) <-> <. b , a >. e. ( ( int ` ( II tX II ) ) ` S ) ) )
108 105 107 ralsn 
 |-  ( A. w e. { a } <. b , w >. e. ( ( int ` ( II tX II ) ) ` S ) <-> <. b , a >. e. ( ( int ` ( II tX II ) ) ` S ) )
109 104 108 sylibr 
 |-  ( ( ph /\ ( a e. ( 0 [,] 1 ) /\ b e. ( 0 [,] 1 ) ) ) -> A. w e. { a } <. b , w >. e. ( ( int ` ( II tX II ) ) ` S ) )
110 109 anassrs 
 |-  ( ( ( ph /\ a e. ( 0 [,] 1 ) ) /\ b e. ( 0 [,] 1 ) ) -> A. w e. { a } <. b , w >. e. ( ( int ` ( II tX II ) ) ` S ) )
111 110 ralrimiva 
 |-  ( ( ph /\ a e. ( 0 [,] 1 ) ) -> A. b e. ( 0 [,] 1 ) A. w e. { a } <. b , w >. e. ( ( int ` ( II tX II ) ) ` S ) )
112 dfss3 
 |-  ( ( ( 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 
 |-  ( u = <. b , w >. -> ( u e. ( ( int ` ( II tX II ) ) ` S ) <-> <. b , w >. e. ( ( int ` ( II tX II ) ) ` S ) ) )
114 113 ralxp 
 |-  ( 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 ) )
115 112 114 bitri 
 |-  ( ( ( 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 ) )
116 111 115 sylibr 
 |-  ( ( ph /\ a e. ( 0 [,] 1 ) ) -> ( ( 0 [,] 1 ) X. { a } ) C_ ( ( int ` ( II tX II ) ) ` S ) )
117 simpr 
 |-  ( ( ph /\ a e. ( 0 [,] 1 ) ) -> a e. ( 0 [,] 1 ) )
118 16 16 21 23 41 116 117 txtube 
 |-  ( ( ph /\ a e. ( 0 [,] 1 ) ) -> E. v e. II ( a e. v /\ ( ( 0 [,] 1 ) X. v ) C_ ( ( int ` ( II tX II ) ) ` S ) ) )
119 38 ntrss2 
 |-  ( ( ( II tX II ) e. Top /\ S C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( ( int ` ( II tX II ) ) ` S ) C_ S )
120 24 37 119 mp2an 
 |-  ( ( int ` ( II tX II ) ) ` S ) C_ S
121 sstr 
 |-  ( ( ( ( 0 [,] 1 ) X. v ) C_ ( ( int ` ( II tX II ) ) ` S ) /\ ( ( int ` ( II tX II ) ) ` S ) C_ S ) -> ( ( 0 [,] 1 ) X. v ) C_ S )
122 120 121 mpan2 
 |-  ( ( ( 0 [,] 1 ) X. v ) C_ ( ( int ` ( II tX II ) ) ` S ) -> ( ( 0 [,] 1 ) X. v ) C_ S )
123 df-xp 
 |-  ( ( 0 [,] 1 ) X. v ) = { <. r , t >. | ( r e. ( 0 [,] 1 ) /\ t e. v ) }
124 123 10 sseq12i 
 |-  ( ( ( 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 ssopab2bw 
 |-  ( { <. 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 
 |-  ( 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 
 |-  ( 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 ) ) )
128 125 126 127 3bitr2i 
 |-  ( { <. 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 ) ) )
129 124 128 bitri 
 |-  ( ( ( 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 ) ) )
130 122 129 sylib 
 |-  ( ( ( 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 
 |-  ( ( 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 ) )
132 131 ralimi 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( ( u X. { a } ) C_ M <-> ( u X. { t } ) C_ M ) <-> ( ( u X. { t } ) C_ M <-> ( u X. { a } ) C_ M ) )
135 134 rexbii 
 |-  ( 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 ) )
136 135 ralbii 
 |-  ( 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 
 |-  ( 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 ) )
138 136 137 sylbi 
 |-  ( 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 ) )
139 133 138 impbid 
 |-  ( 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 ) )
140 132 139 syl 
 |-  ( 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 9 reqabi 
 |-  ( a e. A <-> ( a e. ( 0 [,] 1 ) /\ ( ( 0 [,] 1 ) X. { a } ) C_ M ) )
142 141 baib 
 |-  ( a e. ( 0 [,] 1 ) -> ( a e. A <-> ( ( 0 [,] 1 ) X. { a } ) C_ M ) )
143 142 ad3antlr 
 |-  ( ( ( ( ph /\ a e. ( 0 [,] 1 ) ) /\ v e. II ) /\ t e. v ) -> ( a e. A <-> ( ( 0 [,] 1 ) X. { a } ) C_ M ) )
144 elssuni 
 |-  ( v e. II -> v C_ U. II )
145 144 16 sseqtrrdi 
 |-  ( v e. II -> v C_ ( 0 [,] 1 ) )
146 145 adantl 
 |-  ( ( ( ph /\ a e. ( 0 [,] 1 ) ) /\ v e. II ) -> v C_ ( 0 [,] 1 ) )
147 146 sselda 
 |-  ( ( ( ( ph /\ a e. ( 0 [,] 1 ) ) /\ v e. II ) /\ t e. v ) -> t e. ( 0 [,] 1 ) )
148 sneq 
 |-  ( a = t -> { a } = { t } )
149 148 xpeq2d 
 |-  ( a = t -> ( ( 0 [,] 1 ) X. { a } ) = ( ( 0 [,] 1 ) X. { t } ) )
150 149 sseq1d 
 |-  ( a = t -> ( ( ( 0 [,] 1 ) X. { a } ) C_ M <-> ( ( 0 [,] 1 ) X. { t } ) C_ M ) )
151 150 9 elrab2 
 |-  ( t e. A <-> ( t e. ( 0 [,] 1 ) /\ ( ( 0 [,] 1 ) X. { t } ) C_ M ) )
152 151 baib 
 |-  ( t e. ( 0 [,] 1 ) -> ( t e. A <-> ( ( 0 [,] 1 ) X. { t } ) C_ M ) )
153 147 152 syl 
 |-  ( ( ( ( ph /\ a e. ( 0 [,] 1 ) ) /\ v e. II ) /\ t e. v ) -> ( t e. A <-> ( ( 0 [,] 1 ) X. { t } ) C_ M ) )
154 143 153 bibi12d 
 |-  ( ( ( ( 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 ) ) )
155 140 154 imbitrrid 
 |-  ( ( ( ( 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 ) ) )
156 155 ralimdva 
 |-  ( ( ( 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 ) ) )
157 130 156 syl5 
 |-  ( ( ( 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 ) ) )
158 157 anim2d 
 |-  ( ( ( 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 ) ) ) )
159 158 reximdva 
 |-  ( ( 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 ) ) ) )
160 118 159 mpd 
 |-  ( ( ph /\ a e. ( 0 [,] 1 ) ) -> E. v e. II ( a e. v /\ A. t e. v ( a e. A <-> t e. A ) ) )
161 160 ralrimiva 
 |-  ( 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 
 |-  { a e. ( 0 [,] 1 ) | ( ( 0 [,] 1 ) X. { a } ) C_ M } C_ ( 0 [,] 1 )
163 9 162 eqsstri 
 |-  A C_ ( 0 [,] 1 )
164 16 isclo 
 |-  ( ( 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 ) ) ) )
165 22 163 164 mp2an 
 |-  ( 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 ) ) )
166 161 165 sylibr 
 |-  ( ph -> A e. ( II i^i ( Clsd ` II ) ) )
167 19 166 sselid 
 |-  ( ph -> A e. II )
168 0elunit 
 |-  0 e. ( 0 [,] 1 )
169 168 a1i 
 |-  ( ph -> 0 e. ( 0 [,] 1 ) )
170 relxp 
 |-  Rel ( ( 0 [,] 1 ) X. { 0 } )
171 170 a1i 
 |-  ( ph -> Rel ( ( 0 [,] 1 ) X. { 0 } ) )
172 opelxp 
 |-  ( <. r , a >. e. ( ( 0 [,] 1 ) X. { 0 } ) <-> ( r e. ( 0 [,] 1 ) /\ a e. { 0 } ) )
173 id 
 |-  ( r e. ( 0 [,] 1 ) -> r e. ( 0 [,] 1 ) )
174 opelxpi 
 |-  ( ( r e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) -> <. r , 0 >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
175 173 169 174 syl2anr 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> <. r , 0 >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
176 2 adantr 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> F e. ( C CovMap J ) )
177 3 adantr 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> G e. ( ( II tX II ) Cn J ) )
178 4 adantr 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> P e. B )
179 5 adantr 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> ( F ` P ) = ( 0 G 0 ) )
180 simpr 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> r e. ( 0 [,] 1 ) )
181 168 a1i 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> 0 e. ( 0 [,] 1 ) )
182 1 176 177 178 179 6 7 46 180 181 cvmlift2lem10 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> 0 e. v )
185 11 ad3antrrr 
 |-  ( ( ( ( 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 185 ffnd 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> K Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
187 fnov 
 |-  ( K Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) <-> K = ( b e. ( 0 [,] 1 ) , w e. ( 0 [,] 1 ) |-> ( b K w ) ) )
188 186 187 sylib 
 |-  ( ( ( ( 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 ) ) )
189 188 reseq1d 
 |-  ( ( ( ( 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 } ) ) )
190 simplrl 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> u e. II )
191 elssuni 
 |-  ( u e. II -> u C_ U. II )
192 191 16 sseqtrrdi 
 |-  ( u e. II -> u C_ ( 0 [,] 1 ) )
193 190 192 syl 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> u C_ ( 0 [,] 1 ) )
194 169 snssd 
 |-  ( ph -> { 0 } C_ ( 0 [,] 1 ) )
195 194 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> { 0 } C_ ( 0 [,] 1 ) )
196 resmpo 
 |-  ( ( 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 ) ) )
197 193 195 196 syl2anc 
 |-  ( ( ( ( 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 ) ) )
198 193 sselda 
 |-  ( ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) /\ b e. u ) -> b e. ( 0 [,] 1 ) )
199 simplll 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> ph )
200 1 2 3 4 5 6 7 cvmlift2lem8 
 |-  ( ( ph /\ b e. ( 0 [,] 1 ) ) -> ( b K 0 ) = ( H ` b ) )
201 199 200 sylan 
 |-  ( ( ( ( ( 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 ) )
202 198 201 syldan 
 |-  ( ( ( ( ( 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 ) )
203 elsni 
 |-  ( w e. { 0 } -> w = 0 )
204 203 oveq2d 
 |-  ( w e. { 0 } -> ( b K w ) = ( b K 0 ) )
205 204 eqeq1d 
 |-  ( w e. { 0 } -> ( ( b K w ) = ( H ` b ) <-> ( b K 0 ) = ( H ` b ) ) )
206 202 205 syl5ibrcom 
 |-  ( ( ( ( ( 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 ) ) )
207 206 3impia 
 |-  ( ( ( ( ( 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 ) )
208 207 mpoeq3dva 
 |-  ( ( ( ( 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 ) ) )
209 189 197 208 3eqtrd 
 |-  ( ( ( ( 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 ) ) )
210 eqid 
 |-  ( II |`t u ) = ( II |`t u )
211 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
212 211 a1i 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
213 eqid 
 |-  ( II |`t { 0 } ) = ( II |`t { 0 } )
214 212 212 cnmpt1st 
 |-  ( ( ( ( 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 ) )
215 1 2 3 4 5 6 cvmlift2lem2 
 |-  ( ph -> ( H e. ( II Cn C ) /\ ( F o. H ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( H ` 0 ) = P ) )
216 215 simp1d 
 |-  ( ph -> H e. ( II Cn C ) )
217 199 216 syl 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> H e. ( II Cn C ) )
218 212 212 214 217 cnmpt21f 
 |-  ( ( ( ( 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 ) )
219 210 212 193 213 212 195 218 cnmpt2res 
 |-  ( ( ( ( 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 |`t u ) tX ( II |`t { 0 } ) ) Cn C ) )
220 vex 
 |-  u e. _V
221 snex 
 |-  { 0 } e. _V
222 txrest 
 |-  ( ( ( II e. Top /\ II e. Top ) /\ ( u e. _V /\ { 0 } e. _V ) ) -> ( ( II tX II ) |`t ( u X. { 0 } ) ) = ( ( II |`t u ) tX ( II |`t { 0 } ) ) )
223 22 22 220 221 222 mp4an 
 |-  ( ( II tX II ) |`t ( u X. { 0 } ) ) = ( ( II |`t u ) tX ( II |`t { 0 } ) )
224 223 oveq1i 
 |-  ( ( ( II tX II ) |`t ( u X. { 0 } ) ) Cn C ) = ( ( ( II |`t u ) tX ( II |`t { 0 } ) ) Cn C )
225 219 224 eleqtrrdi 
 |-  ( ( ( ( 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 ) )
226 209 225 eqeltrd 
 |-  ( ( ( ( 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 ) )
227 sneq 
 |-  ( w = 0 -> { w } = { 0 } )
228 227 xpeq2d 
 |-  ( w = 0 -> ( u X. { w } ) = ( u X. { 0 } ) )
229 228 reseq2d 
 |-  ( w = 0 -> ( K |` ( u X. { w } ) ) = ( K |` ( u X. { 0 } ) ) )
230 228 oveq2d 
 |-  ( w = 0 -> ( ( II tX II ) |`t ( u X. { w } ) ) = ( ( II tX II ) |`t ( u X. { 0 } ) ) )
231 230 oveq1d 
 |-  ( w = 0 -> ( ( ( II tX II ) |`t ( u X. { w } ) ) Cn C ) = ( ( ( II tX II ) |`t ( u X. { 0 } ) ) Cn C ) )
232 229 231 eleq12d 
 |-  ( 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 ) ) )
233 232 rspcev 
 |-  ( ( 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 ) )
234 184 226 233 syl2anc 
 |-  ( ( ( ( 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 ) )
235 opelxpi 
 |-  ( ( r e. u /\ 0 e. v ) -> <. r , 0 >. e. ( u X. v ) )
236 235 adantl 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> <. r , 0 >. e. ( u X. v ) )
237 simplrr 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> v e. II )
238 237 145 syl 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> v C_ ( 0 [,] 1 ) )
239 xpss12 
 |-  ( ( u C_ ( 0 [,] 1 ) /\ v C_ ( 0 [,] 1 ) ) -> ( u X. v ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
240 193 238 239 syl2anc 
 |-  ( ( ( ( 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 ) ) )
241 38 restuni 
 |-  ( ( ( 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 ) ) )
242 24 240 241 sylancr 
 |-  ( ( ( ( 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 ) ) )
243 236 242 eleqtrd 
 |-  ( ( ( ( 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 ) ) )
244 eqid 
 |-  U. ( ( II tX II ) |`t ( u X. v ) ) = U. ( ( II tX II ) |`t ( u X. v ) )
245 244 cncnpi 
 |-  ( ( ( 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 >. ) )
246 245 expcom 
 |-  ( <. 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 >. ) ) )
247 243 246 syl 
 |-  ( ( ( ( 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 >. ) ) )
248 24 a1i 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> ( II tX II ) e. Top )
249 22 a1i 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> II e. Top )
250 249 249 190 237 55 syl22anc 
 |-  ( ( ( ( ph /\ r e. ( 0 [,] 1 ) ) /\ ( u e. II /\ v e. II ) ) /\ ( r e. u /\ 0 e. v ) ) -> ( u X. v ) e. ( II tX II ) )
251 isopn3i 
 |-  ( ( ( II tX II ) e. Top /\ ( u X. v ) e. ( II tX II ) ) -> ( ( int ` ( II tX II ) ) ` ( u X. v ) ) = ( u X. v ) )
252 24 250 251 sylancr 
 |-  ( ( ( ( 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 ) )
253 236 252 eleqtrrd 
 |-  ( ( ( ( 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 ) ) )
254 38 1 cnprest 
 |-  ( ( ( ( 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 >. ) ) )
255 248 240 253 185 254 syl22anc 
 |-  ( ( ( ( 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 >. ) ) )
256 247 255 sylibrd 
 |-  ( ( ( ( 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 >. ) ) )
257 234 256 embantd 
 |-  ( ( ( ( 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 >. ) ) )
258 257 expimpd 
 |-  ( ( ( 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 >. ) ) )
259 183 258 biimtrid 
 |-  ( ( ( 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 >. ) ) )
260 259 rexlimdvva 
 |-  ( ( 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 >. ) ) )
261 182 260 mpd 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> K e. ( ( ( II tX II ) CnP C ) ` <. r , 0 >. ) )
262 fveq2 
 |-  ( z = <. r , 0 >. -> ( ( ( II tX II ) CnP C ) ` z ) = ( ( ( II tX II ) CnP C ) ` <. r , 0 >. ) )
263 262 eleq2d 
 |-  ( z = <. r , 0 >. -> ( K e. ( ( ( II tX II ) CnP C ) ` z ) <-> K e. ( ( ( II tX II ) CnP C ) ` <. r , 0 >. ) ) )
264 263 8 elrab2 
 |-  ( <. r , 0 >. e. M <-> ( <. r , 0 >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) /\ K e. ( ( ( II tX II ) CnP C ) ` <. r , 0 >. ) ) )
265 175 261 264 sylanbrc 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> <. r , 0 >. e. M )
266 elsni 
 |-  ( a e. { 0 } -> a = 0 )
267 266 opeq2d 
 |-  ( a e. { 0 } -> <. r , a >. = <. r , 0 >. )
268 267 eleq1d 
 |-  ( a e. { 0 } -> ( <. r , a >. e. M <-> <. r , 0 >. e. M ) )
269 265 268 syl5ibrcom 
 |-  ( ( ph /\ r e. ( 0 [,] 1 ) ) -> ( a e. { 0 } -> <. r , a >. e. M ) )
270 269 expimpd 
 |-  ( ph -> ( ( r e. ( 0 [,] 1 ) /\ a e. { 0 } ) -> <. r , a >. e. M ) )
271 172 270 biimtrid 
 |-  ( ph -> ( <. r , a >. e. ( ( 0 [,] 1 ) X. { 0 } ) -> <. r , a >. e. M ) )
272 171 271 relssdv 
 |-  ( ph -> ( ( 0 [,] 1 ) X. { 0 } ) C_ M )
273 sneq 
 |-  ( a = 0 -> { a } = { 0 } )
274 273 xpeq2d 
 |-  ( a = 0 -> ( ( 0 [,] 1 ) X. { a } ) = ( ( 0 [,] 1 ) X. { 0 } ) )
275 274 sseq1d 
 |-  ( a = 0 -> ( ( ( 0 [,] 1 ) X. { a } ) C_ M <-> ( ( 0 [,] 1 ) X. { 0 } ) C_ M ) )
276 275 9 elrab2 
 |-  ( 0 e. A <-> ( 0 e. ( 0 [,] 1 ) /\ ( ( 0 [,] 1 ) X. { 0 } ) C_ M ) )
277 169 272 276 sylanbrc 
 |-  ( ph -> 0 e. A )
278 277 ne0d 
 |-  ( ph -> A =/= (/) )
279 inss2 
 |-  ( II i^i ( Clsd ` II ) ) C_ ( Clsd ` II )
280 279 166 sselid 
 |-  ( ph -> A e. ( Clsd ` II ) )
281 16 18 167 278 280 connclo 
 |-  ( ph -> A = ( 0 [,] 1 ) )
282 281 9 eqtr3di 
 |-  ( ph -> ( 0 [,] 1 ) = { a e. ( 0 [,] 1 ) | ( ( 0 [,] 1 ) X. { a } ) C_ M } )
283 rabid2 
 |-  ( ( 0 [,] 1 ) = { a e. ( 0 [,] 1 ) | ( ( 0 [,] 1 ) X. { a } ) C_ M } <-> A. a e. ( 0 [,] 1 ) ( ( 0 [,] 1 ) X. { a } ) C_ M )
284 282 283 sylib 
 |-  ( ph -> A. a e. ( 0 [,] 1 ) ( ( 0 [,] 1 ) X. { a } ) C_ M )
285 iunss 
 |-  ( U_ a e. ( 0 [,] 1 ) ( ( 0 [,] 1 ) X. { a } ) C_ M <-> A. a e. ( 0 [,] 1 ) ( ( 0 [,] 1 ) X. { a } ) C_ M )
286 284 285 sylibr 
 |-  ( ph -> U_ a e. ( 0 [,] 1 ) ( ( 0 [,] 1 ) X. { a } ) C_ M )
287 15 286 eqsstrid 
 |-  ( ph -> ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ M )
288 287 8 sseqtrdi 
 |-  ( ph -> ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) } )
289 ssrab 
 |-  ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) } <-> ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) /\ A. z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) K e. ( ( ( II tX II ) CnP C ) ` z ) ) )
290 289 simprbi 
 |-  ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ { z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) | K e. ( ( ( II tX II ) CnP C ) ` z ) } -> A. z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) K e. ( ( ( II tX II ) CnP C ) ` z ) )
291 288 290 syl 
 |-  ( ph -> A. z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) K e. ( ( ( II tX II ) CnP C ) ` z ) )
292 txtopon 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ II e. ( TopOn ` ( 0 [,] 1 ) ) ) -> ( II tX II ) e. ( TopOn ` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
293 211 211 292 mp2an 
 |-  ( II tX II ) e. ( TopOn ` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
294 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
295 2 294 syl 
 |-  ( ph -> C e. Top )
296 1 toptopon 
 |-  ( C e. Top <-> C e. ( TopOn ` B ) )
297 295 296 sylib 
 |-  ( ph -> C e. ( TopOn ` B ) )
298 cncnp 
 |-  ( ( ( II tX II ) e. ( TopOn ` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) /\ C e. ( TopOn ` B ) ) -> ( K e. ( ( II tX II ) Cn C ) <-> ( K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B /\ A. z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) K e. ( ( ( II tX II ) CnP C ) ` z ) ) ) )
299 293 297 298 sylancr 
 |-  ( ph -> ( K e. ( ( II tX II ) Cn C ) <-> ( K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B /\ A. z e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) K e. ( ( ( II tX II ) CnP C ) ` z ) ) ) )
300 11 291 299 mpbir2and 
 |-  ( ph -> K e. ( ( II tX II ) Cn C ) )