Metamath Proof Explorer

Theorem cvmlift2lem9

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 ) )
cvmlift2lem10.s 
|- S = ( 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 ) ) ) ) } )
cvmlift2lem9.1 
|- ( ph -> ( X G Y ) e. M )
cvmlift2lem9.2 
|- ( ph -> T e. ( S ` M ) )
cvmlift2lem9.3 
|- ( ph -> U e. II )
cvmlift2lem9.4 
|- ( ph -> V e. II )
cvmlift2lem9.5 
|- ( ph -> ( II |`t U ) e. Conn )
cvmlift2lem9.6 
|- ( ph -> ( II |`t V ) e. Conn )
cvmlift2lem9.7 
|- ( ph -> X e. U )
cvmlift2lem9.8 
|- ( ph -> Y e. V )
cvmlift2lem9.9 
|- ( ph -> ( U X. V ) C_ ( `' G " M ) )
cvmlift2lem9.10 
|- ( ph -> Z e. V )
cvmlift2lem9.11 
|- ( ph -> ( K |` ( U X. { Z } ) ) e. ( ( ( II tX II ) |`t ( U X. { Z } ) ) Cn C ) )
cvmlift2lem9.w 
|- W = ( iota_ b e. T ( X K Y ) e. b )
Assertion cvmlift2lem9 
|- ( ph -> ( K |` ( U X. V ) ) e. ( ( ( II tX II ) |`t ( U X. V ) ) 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 cvmlift2lem10.s 
 |-  S = ( 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 ) ) ) ) } )
9 cvmlift2lem9.1 
 |-  ( ph -> ( X G Y ) e. M )
10 cvmlift2lem9.2 
 |-  ( ph -> T e. ( S ` M ) )
11 cvmlift2lem9.3 
 |-  ( ph -> U e. II )
12 cvmlift2lem9.4 
 |-  ( ph -> V e. II )
13 cvmlift2lem9.5 
 |-  ( ph -> ( II |`t U ) e. Conn )
14 cvmlift2lem9.6 
 |-  ( ph -> ( II |`t V ) e. Conn )
15 cvmlift2lem9.7 
 |-  ( ph -> X e. U )
16 cvmlift2lem9.8 
 |-  ( ph -> Y e. V )
17 cvmlift2lem9.9 
 |-  ( ph -> ( U X. V ) C_ ( `' G " M ) )
18 cvmlift2lem9.10 
 |-  ( ph -> Z e. V )
19 cvmlift2lem9.11 
 |-  ( ph -> ( K |` ( U X. { Z } ) ) e. ( ( ( II tX II ) |`t ( U X. { Z } ) ) Cn C ) )
20 cvmlift2lem9.w 
 |-  W = ( iota_ b e. T ( X K Y ) e. b )
21 iitop 
 |-  II e. Top
22 iiuni 
 |-  ( 0 [,] 1 ) = U. II
23 21 21 22 22 txunii 
 |-  ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) = U. ( II tX II )
24 1 2 3 4 5 6 7 cvmlift2lem5 
 |-  ( ph -> K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B )
25 1 2 3 4 5 6 7 cvmlift2lem7 
 |-  ( ph -> ( F o. K ) = G )
26 25 3 eqeltrd 
 |-  ( ph -> ( F o. K ) e. ( ( II tX II ) Cn J ) )
27 21 21 txtopi 
 |-  ( II tX II ) e. Top
28 27 a1i 
 |-  ( ph -> ( II tX II ) e. Top )
29 elssuni 
 |-  ( U e. II -> U C_ U. II )
30 29 22 sseqtrrdi 
 |-  ( U e. II -> U C_ ( 0 [,] 1 ) )
31 11 30 syl 
 |-  ( ph -> U C_ ( 0 [,] 1 ) )
32 31 15 sseldd 
 |-  ( ph -> X e. ( 0 [,] 1 ) )
33 elssuni 
 |-  ( V e. II -> V C_ U. II )
34 33 22 sseqtrrdi 
 |-  ( V e. II -> V C_ ( 0 [,] 1 ) )
35 12 34 syl 
 |-  ( ph -> V C_ ( 0 [,] 1 ) )
36 35 16 sseldd 
 |-  ( ph -> Y e. ( 0 [,] 1 ) )
37 opelxpi 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y e. ( 0 [,] 1 ) ) -> <. X , Y >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
38 32 36 37 syl2anc 
 |-  ( ph -> <. X , Y >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
39 24 32 36 fovrnd 
 |-  ( ph -> ( X K Y ) e. B )
40 fvco3 
 |-  ( ( K : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> B /\ <. X , Y >. e. ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( ( F o. K ) ` <. X , Y >. ) = ( F ` ( K ` <. X , Y >. ) ) )
41 24 38 40 syl2anc 
 |-  ( ph -> ( ( F o. K ) ` <. X , Y >. ) = ( F ` ( K ` <. X , Y >. ) ) )
42 25 fveq1d 
 |-  ( ph -> ( ( F o. K ) ` <. X , Y >. ) = ( G ` <. X , Y >. ) )
43 41 42 eqtr3d 
 |-  ( ph -> ( F ` ( K ` <. X , Y >. ) ) = ( G ` <. X , Y >. ) )
44 df-ov 
 |-  ( X K Y ) = ( K ` <. X , Y >. )
45 44 fveq2i 
 |-  ( F ` ( X K Y ) ) = ( F ` ( K ` <. X , Y >. ) )
46 df-ov 
 |-  ( X G Y ) = ( G ` <. X , Y >. )
47 43 45 46 3eqtr4g 
 |-  ( ph -> ( F ` ( X K Y ) ) = ( X G Y ) )
48 47 9 eqeltrd 
 |-  ( ph -> ( F ` ( X K Y ) ) e. M )
49 8 1 20 cvmsiota 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` M ) /\ ( X K Y ) e. B /\ ( F ` ( X K Y ) ) e. M ) ) -> ( W e. T /\ ( X K Y ) e. W ) )
50 2 10 39 48 49 syl13anc 
 |-  ( ph -> ( W e. T /\ ( X K Y ) e. W ) )
51 44 eleq1i 
 |-  ( ( X K Y ) e. W <-> ( K ` <. X , Y >. ) e. W )
52 51 anbi2i 
 |-  ( ( W e. T /\ ( X K Y ) e. W ) <-> ( W e. T /\ ( K ` <. X , Y >. ) e. W ) )
53 50 52 sylib 
 |-  ( ph -> ( W e. T /\ ( K ` <. X , Y >. ) e. W ) )
54 xpss12 
 |-  ( ( U C_ ( 0 [,] 1 ) /\ V C_ ( 0 [,] 1 ) ) -> ( U X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
55 31 35 54 syl2anc 
 |-  ( ph -> ( U X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
56 snidg 
 |-  ( m e. U -> m e. { m } )
57 56 ad2antrl 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> m e. { m } )
58 simprr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> n e. V )
59 ovres 
 |-  ( ( m e. { m } /\ n e. V ) -> ( m ( K |` ( { m } X. V ) ) n ) = ( m K n ) )
60 57 58 59 syl2anc 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( m ( K |` ( { m } X. V ) ) n ) = ( m K n ) )
61 eqid 
 |-  U. ( ( II tX II ) |`t ( { m } X. V ) ) = U. ( ( II tX II ) |`t ( { m } X. V ) )
62 21 a1i 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> II e. Top )
63 snex 
 |-  { m } e. _V
64 63 a1i 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> { m } e. _V )
65 12 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> V e. II )
66 txrest 
 |-  ( ( ( II e. Top /\ II e. Top ) /\ ( { m } e. _V /\ V e. II ) ) -> ( ( II tX II ) |`t ( { m } X. V ) ) = ( ( II |`t { m } ) tX ( II |`t V ) ) )
67 62 62 64 65 66 syl22anc 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( II tX II ) |`t ( { m } X. V ) ) = ( ( II |`t { m } ) tX ( II |`t V ) ) )
68 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
69 31 sselda 
 |-  ( ( ph /\ m e. U ) -> m e. ( 0 [,] 1 ) )
70 69 adantrr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> m e. ( 0 [,] 1 ) )
71 restsn2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ m e. ( 0 [,] 1 ) ) -> ( II |`t { m } ) = ~P { m } )
72 68 70 71 sylancr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( II |`t { m } ) = ~P { m } )
73 pwsn 
 |-  ~P { m } = { (/) , { m } }
74 indisconn 
 |-  { (/) , { m } } e. Conn
75 73 74 eqeltri 
 |-  ~P { m } e. Conn
76 72 75 eqeltrdi 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( II |`t { m } ) e. Conn )
77 14 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( II |`t V ) e. Conn )
78 txconn 
 |-  ( ( ( II |`t { m } ) e. Conn /\ ( II |`t V ) e. Conn ) -> ( ( II |`t { m } ) tX ( II |`t V ) ) e. Conn )
79 76 77 78 syl2anc 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( II |`t { m } ) tX ( II |`t V ) ) e. Conn )
80 67 79 eqeltrd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( II tX II ) |`t ( { m } X. V ) ) e. Conn )
81 1 2 3 4 5 6 7 cvmlift2lem6 
 |-  ( ( ph /\ m e. ( 0 [,] 1 ) ) -> ( K |` ( { m } X. ( 0 [,] 1 ) ) ) e. ( ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) Cn C ) )
82 70 81 syldan 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( K |` ( { m } X. ( 0 [,] 1 ) ) ) e. ( ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) Cn C ) )
83 35 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> V C_ ( 0 [,] 1 ) )
84 xpss2 
 |-  ( V C_ ( 0 [,] 1 ) -> ( { m } X. V ) C_ ( { m } X. ( 0 [,] 1 ) ) )
85 83 84 syl 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( { m } X. V ) C_ ( { m } X. ( 0 [,] 1 ) ) )
86 70 snssd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> { m } C_ ( 0 [,] 1 ) )
87 xpss1 
 |-  ( { m } C_ ( 0 [,] 1 ) -> ( { m } X. ( 0 [,] 1 ) ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
88 86 87 syl 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( { m } X. ( 0 [,] 1 ) ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
89 23 restuni 
 |-  ( ( ( II tX II ) e. Top /\ ( { m } X. ( 0 [,] 1 ) ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( { m } X. ( 0 [,] 1 ) ) = U. ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) )
90 27 88 89 sylancr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( { m } X. ( 0 [,] 1 ) ) = U. ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) )
91 85 90 sseqtrd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( { m } X. V ) C_ U. ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) )
92 eqid 
 |-  U. ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) = U. ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) )
93 92 cnrest 
 |-  ( ( ( K |` ( { m } X. ( 0 [,] 1 ) ) ) e. ( ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) Cn C ) /\ ( { m } X. V ) C_ U. ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) ) -> ( ( K |` ( { m } X. ( 0 [,] 1 ) ) ) |` ( { m } X. V ) ) e. ( ( ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) |`t ( { m } X. V ) ) Cn C ) )
94 82 91 93 syl2anc 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( K |` ( { m } X. ( 0 [,] 1 ) ) ) |` ( { m } X. V ) ) e. ( ( ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) |`t ( { m } X. V ) ) Cn C ) )
95 85 resabs1d 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( K |` ( { m } X. ( 0 [,] 1 ) ) ) |` ( { m } X. V ) ) = ( K |` ( { m } X. V ) ) )
96 27 a1i 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( II tX II ) e. Top )
97 ovex 
 |-  ( 0 [,] 1 ) e. _V
98 63 97 xpex 
 |-  ( { m } X. ( 0 [,] 1 ) ) e. _V
99 98 a1i 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( { m } X. ( 0 [,] 1 ) ) e. _V )
100 restabs 
 |-  ( ( ( II tX II ) e. Top /\ ( { m } X. V ) C_ ( { m } X. ( 0 [,] 1 ) ) /\ ( { m } X. ( 0 [,] 1 ) ) e. _V ) -> ( ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) |`t ( { m } X. V ) ) = ( ( II tX II ) |`t ( { m } X. V ) ) )
101 96 85 99 100 syl3anc 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) |`t ( { m } X. V ) ) = ( ( II tX II ) |`t ( { m } X. V ) ) )
102 101 oveq1d 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( ( ( II tX II ) |`t ( { m } X. ( 0 [,] 1 ) ) ) |`t ( { m } X. V ) ) Cn C ) = ( ( ( II tX II ) |`t ( { m } X. V ) ) Cn C ) )
103 94 95 102 3eltr3d 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( K |` ( { m } X. V ) ) e. ( ( ( II tX II ) |`t ( { m } X. V ) ) Cn C ) )
104 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
105 2 104 syl 
 |-  ( ph -> C e. Top )
106 105 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> C e. Top )
107 1 toptopon 
 |-  ( C e. Top <-> C e. ( TopOn ` B ) )
108 106 107 sylib 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> C e. ( TopOn ` B ) )
109 df-ima 
 |-  ( K " ( { m } X. V ) ) = ran ( K |` ( { m } X. V ) )
110 simprl 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> m e. U )
111 110 snssd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> { m } C_ U )
112 xpss1 
 |-  ( { m } C_ U -> ( { m } X. V ) C_ ( U X. V ) )
113 imass2 
 |-  ( ( { m } X. V ) C_ ( U X. V ) -> ( K " ( { m } X. V ) ) C_ ( K " ( U X. V ) ) )
114 111 112 113 3syl 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( K " ( { m } X. V ) ) C_ ( K " ( U X. V ) ) )
115 imaco 
 |-  ( ( `' K o. `' F ) " M ) = ( `' K " ( `' F " M ) )
116 cnvco 
 |-  `' ( F o. K ) = ( `' K o. `' F )
117 25 cnveqd 
 |-  ( ph -> `' ( F o. K ) = `' G )
118 116 117 eqtr3id 
 |-  ( ph -> ( `' K o. `' F ) = `' G )
119 118 imaeq1d 
 |-  ( ph -> ( ( `' K o. `' F ) " M ) = ( `' G " M ) )
120 115 119 eqtr3id 
 |-  ( ph -> ( `' K " ( `' F " M ) ) = ( `' G " M ) )
121 17 120 sseqtrrd 
 |-  ( ph -> ( U X. V ) C_ ( `' K " ( `' F " M ) ) )
122 24 ffund 
 |-  ( ph -> Fun K )
123 24 fdmd 
 |-  ( ph -> dom K = ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
124 55 123 sseqtrrd 
 |-  ( ph -> ( U X. V ) C_ dom K )
125 funimass3 
 |-  ( ( Fun K /\ ( U X. V ) C_ dom K ) -> ( ( K " ( U X. V ) ) C_ ( `' F " M ) <-> ( U X. V ) C_ ( `' K " ( `' F " M ) ) ) )
126 122 124 125 syl2anc 
 |-  ( ph -> ( ( K " ( U X. V ) ) C_ ( `' F " M ) <-> ( U X. V ) C_ ( `' K " ( `' F " M ) ) ) )
127 121 126 mpbird 
 |-  ( ph -> ( K " ( U X. V ) ) C_ ( `' F " M ) )
128 127 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( K " ( U X. V ) ) C_ ( `' F " M ) )
129 114 128 sstrd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( K " ( { m } X. V ) ) C_ ( `' F " M ) )
130 109 129 eqsstrrid 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ran ( K |` ( { m } X. V ) ) C_ ( `' F " M ) )
131 cnvimass 
 |-  ( `' F " M ) C_ dom F
132 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
133 2 132 syl 
 |-  ( ph -> F e. ( C Cn J ) )
134 eqid 
 |-  U. J = U. J
135 1 134 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> U. J )
136 fdm 
 |-  ( F : B --> U. J -> dom F = B )
137 133 135 136 3syl 
 |-  ( ph -> dom F = B )
138 131 137 sseqtrid 
 |-  ( ph -> ( `' F " M ) C_ B )
139 138 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( `' F " M ) C_ B )
140 cnrest2 
 |-  ( ( C e. ( TopOn ` B ) /\ ran ( K |` ( { m } X. V ) ) C_ ( `' F " M ) /\ ( `' F " M ) C_ B ) -> ( ( K |` ( { m } X. V ) ) e. ( ( ( II tX II ) |`t ( { m } X. V ) ) Cn C ) <-> ( K |` ( { m } X. V ) ) e. ( ( ( II tX II ) |`t ( { m } X. V ) ) Cn ( C |`t ( `' F " M ) ) ) ) )
141 108 130 139 140 syl3anc 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( K |` ( { m } X. V ) ) e. ( ( ( II tX II ) |`t ( { m } X. V ) ) Cn C ) <-> ( K |` ( { m } X. V ) ) e. ( ( ( II tX II ) |`t ( { m } X. V ) ) Cn ( C |`t ( `' F " M ) ) ) ) )
142 103 141 mpbid 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( K |` ( { m } X. V ) ) e. ( ( ( II tX II ) |`t ( { m } X. V ) ) Cn ( C |`t ( `' F " M ) ) ) )
143 8 cvmsss 
 |-  ( T e. ( S ` M ) -> T C_ C )
144 10 143 syl 
 |-  ( ph -> T C_ C )
145 50 simpld 
 |-  ( ph -> W e. T )
146 144 145 sseldd 
 |-  ( ph -> W e. C )
147 elssuni 
 |-  ( W e. T -> W C_ U. T )
148 145 147 syl 
 |-  ( ph -> W C_ U. T )
149 8 cvmsuni 
 |-  ( T e. ( S ` M ) -> U. T = ( `' F " M ) )
150 10 149 syl 
 |-  ( ph -> U. T = ( `' F " M ) )
151 148 150 sseqtrd 
 |-  ( ph -> W C_ ( `' F " M ) )
152 8 cvmsrcl 
 |-  ( T e. ( S ` M ) -> M e. J )
153 10 152 syl 
 |-  ( ph -> M e. J )
154 cnima 
 |-  ( ( F e. ( C Cn J ) /\ M e. J ) -> ( `' F " M ) e. C )
155 133 153 154 syl2anc 
 |-  ( ph -> ( `' F " M ) e. C )
156 restopn2 
 |-  ( ( C e. Top /\ ( `' F " M ) e. C ) -> ( W e. ( C |`t ( `' F " M ) ) <-> ( W e. C /\ W C_ ( `' F " M ) ) ) )
157 105 155 156 syl2anc 
 |-  ( ph -> ( W e. ( C |`t ( `' F " M ) ) <-> ( W e. C /\ W C_ ( `' F " M ) ) ) )
158 146 151 157 mpbir2and 
 |-  ( ph -> W e. ( C |`t ( `' F " M ) ) )
159 158 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> W e. ( C |`t ( `' F " M ) ) )
160 8 cvmscld 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` M ) /\ W e. T ) -> W e. ( Clsd ` ( C |`t ( `' F " M ) ) ) )
161 2 10 145 160 syl3anc 
 |-  ( ph -> W e. ( Clsd ` ( C |`t ( `' F " M ) ) ) )
162 161 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> W e. ( Clsd ` ( C |`t ( `' F " M ) ) ) )
163 18 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> Z e. V )
164 opelxpi 
 |-  ( ( m e. { m } /\ Z e. V ) -> <. m , Z >. e. ( { m } X. V ) )
165 57 163 164 syl2anc 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> <. m , Z >. e. ( { m } X. V ) )
166 85 88 sstrd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( { m } X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
167 23 restuni 
 |-  ( ( ( II tX II ) e. Top /\ ( { m } X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( { m } X. V ) = U. ( ( II tX II ) |`t ( { m } X. V ) ) )
168 27 166 167 sylancr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( { m } X. V ) = U. ( ( II tX II ) |`t ( { m } X. V ) ) )
169 165 168 eleqtrd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> <. m , Z >. e. U. ( ( II tX II ) |`t ( { m } X. V ) ) )
170 df-ov 
 |-  ( m ( K |` ( { m } X. V ) ) Z ) = ( ( K |` ( { m } X. V ) ) ` <. m , Z >. )
171 ovres 
 |-  ( ( m e. { m } /\ Z e. V ) -> ( m ( K |` ( { m } X. V ) ) Z ) = ( m K Z ) )
172 57 163 171 syl2anc 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( m ( K |` ( { m } X. V ) ) Z ) = ( m K Z ) )
173 snidg 
 |-  ( Z e. V -> Z e. { Z } )
174 18 173 syl 
 |-  ( ph -> Z e. { Z } )
175 174 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> Z e. { Z } )
176 ovres 
 |-  ( ( m e. U /\ Z e. { Z } ) -> ( m ( K |` ( U X. { Z } ) ) Z ) = ( m K Z ) )
177 110 175 176 syl2anc 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( m ( K |` ( U X. { Z } ) ) Z ) = ( m K Z ) )
178 172 177 eqtr4d 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( m ( K |` ( { m } X. V ) ) Z ) = ( m ( K |` ( U X. { Z } ) ) Z ) )
179 170 178 eqtr3id 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( K |` ( { m } X. V ) ) ` <. m , Z >. ) = ( m ( K |` ( U X. { Z } ) ) Z ) )
180 eqid 
 |-  U. ( ( II tX II ) |`t ( U X. { Z } ) ) = U. ( ( II tX II ) |`t ( U X. { Z } ) )
181 21 a1i 
 |-  ( ph -> II e. Top )
182 snex 
 |-  { Z } e. _V
183 182 a1i 
 |-  ( ph -> { Z } e. _V )
184 txrest 
 |-  ( ( ( II e. Top /\ II e. Top ) /\ ( U e. II /\ { Z } e. _V ) ) -> ( ( II tX II ) |`t ( U X. { Z } ) ) = ( ( II |`t U ) tX ( II |`t { Z } ) ) )
185 181 181 11 183 184 syl22anc 
 |-  ( ph -> ( ( II tX II ) |`t ( U X. { Z } ) ) = ( ( II |`t U ) tX ( II |`t { Z } ) ) )
186 35 18 sseldd 
 |-  ( ph -> Z e. ( 0 [,] 1 ) )
187 restsn2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ Z e. ( 0 [,] 1 ) ) -> ( II |`t { Z } ) = ~P { Z } )
188 68 186 187 sylancr 
 |-  ( ph -> ( II |`t { Z } ) = ~P { Z } )
189 pwsn 
 |-  ~P { Z } = { (/) , { Z } }
190 indisconn 
 |-  { (/) , { Z } } e. Conn
191 189 190 eqeltri 
 |-  ~P { Z } e. Conn
192 188 191 eqeltrdi 
 |-  ( ph -> ( II |`t { Z } ) e. Conn )
193 txconn 
 |-  ( ( ( II |`t U ) e. Conn /\ ( II |`t { Z } ) e. Conn ) -> ( ( II |`t U ) tX ( II |`t { Z } ) ) e. Conn )
194 13 192 193 syl2anc 
 |-  ( ph -> ( ( II |`t U ) tX ( II |`t { Z } ) ) e. Conn )
195 185 194 eqeltrd 
 |-  ( ph -> ( ( II tX II ) |`t ( U X. { Z } ) ) e. Conn )
196 105 107 sylib 
 |-  ( ph -> C e. ( TopOn ` B ) )
197 df-ima 
 |-  ( K " ( U X. { Z } ) ) = ran ( K |` ( U X. { Z } ) )
198 18 snssd 
 |-  ( ph -> { Z } C_ V )
199 xpss2 
 |-  ( { Z } C_ V -> ( U X. { Z } ) C_ ( U X. V ) )
200 imass2 
 |-  ( ( U X. { Z } ) C_ ( U X. V ) -> ( K " ( U X. { Z } ) ) C_ ( K " ( U X. V ) ) )
201 198 199 200 3syl 
 |-  ( ph -> ( K " ( U X. { Z } ) ) C_ ( K " ( U X. V ) ) )
202 201 127 sstrd 
 |-  ( ph -> ( K " ( U X. { Z } ) ) C_ ( `' F " M ) )
203 197 202 eqsstrrid 
 |-  ( ph -> ran ( K |` ( U X. { Z } ) ) C_ ( `' F " M ) )
204 cnrest2 
 |-  ( ( C e. ( TopOn ` B ) /\ ran ( K |` ( U X. { Z } ) ) C_ ( `' F " M ) /\ ( `' F " M ) C_ B ) -> ( ( K |` ( U X. { Z } ) ) e. ( ( ( II tX II ) |`t ( U X. { Z } ) ) Cn C ) <-> ( K |` ( U X. { Z } ) ) e. ( ( ( II tX II ) |`t ( U X. { Z } ) ) Cn ( C |`t ( `' F " M ) ) ) ) )
205 196 203 138 204 syl3anc 
 |-  ( ph -> ( ( K |` ( U X. { Z } ) ) e. ( ( ( II tX II ) |`t ( U X. { Z } ) ) Cn C ) <-> ( K |` ( U X. { Z } ) ) e. ( ( ( II tX II ) |`t ( U X. { Z } ) ) Cn ( C |`t ( `' F " M ) ) ) ) )
206 19 205 mpbid 
 |-  ( ph -> ( K |` ( U X. { Z } ) ) e. ( ( ( II tX II ) |`t ( U X. { Z } ) ) Cn ( C |`t ( `' F " M ) ) ) )
207 opelxpi 
 |-  ( ( X e. U /\ Z e. { Z } ) -> <. X , Z >. e. ( U X. { Z } ) )
208 15 174 207 syl2anc 
 |-  ( ph -> <. X , Z >. e. ( U X. { Z } ) )
209 186 snssd 
 |-  ( ph -> { Z } C_ ( 0 [,] 1 ) )
210 xpss12 
 |-  ( ( U C_ ( 0 [,] 1 ) /\ { Z } C_ ( 0 [,] 1 ) ) -> ( U X. { Z } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
211 31 209 210 syl2anc 
 |-  ( ph -> ( U X. { Z } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
212 23 restuni 
 |-  ( ( ( II tX II ) e. Top /\ ( U X. { Z } ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( U X. { Z } ) = U. ( ( II tX II ) |`t ( U X. { Z } ) ) )
213 27 211 212 sylancr 
 |-  ( ph -> ( U X. { Z } ) = U. ( ( II tX II ) |`t ( U X. { Z } ) ) )
214 208 213 eleqtrd 
 |-  ( ph -> <. X , Z >. e. U. ( ( II tX II ) |`t ( U X. { Z } ) ) )
215 df-ov 
 |-  ( X ( K |` ( U X. { Z } ) ) Z ) = ( ( K |` ( U X. { Z } ) ) ` <. X , Z >. )
216 ovres 
 |-  ( ( X e. U /\ Z e. { Z } ) -> ( X ( K |` ( U X. { Z } ) ) Z ) = ( X K Z ) )
217 15 174 216 syl2anc 
 |-  ( ph -> ( X ( K |` ( U X. { Z } ) ) Z ) = ( X K Z ) )
218 snidg 
 |-  ( X e. U -> X e. { X } )
219 15 218 syl 
 |-  ( ph -> X e. { X } )
220 ovres 
 |-  ( ( X e. { X } /\ Z e. V ) -> ( X ( K |` ( { X } X. V ) ) Z ) = ( X K Z ) )
221 219 18 220 syl2anc 
 |-  ( ph -> ( X ( K |` ( { X } X. V ) ) Z ) = ( X K Z ) )
222 217 221 eqtr4d 
 |-  ( ph -> ( X ( K |` ( U X. { Z } ) ) Z ) = ( X ( K |` ( { X } X. V ) ) Z ) )
223 215 222 eqtr3id 
 |-  ( ph -> ( ( K |` ( U X. { Z } ) ) ` <. X , Z >. ) = ( X ( K |` ( { X } X. V ) ) Z ) )
224 eqid 
 |-  U. ( ( II tX II ) |`t ( { X } X. V ) ) = U. ( ( II tX II ) |`t ( { X } X. V ) )
225 snex 
 |-  { X } e. _V
226 225 a1i 
 |-  ( ph -> { X } e. _V )
227 txrest 
 |-  ( ( ( II e. Top /\ II e. Top ) /\ ( { X } e. _V /\ V e. II ) ) -> ( ( II tX II ) |`t ( { X } X. V ) ) = ( ( II |`t { X } ) tX ( II |`t V ) ) )
228 181 181 226 12 227 syl22anc 
 |-  ( ph -> ( ( II tX II ) |`t ( { X } X. V ) ) = ( ( II |`t { X } ) tX ( II |`t V ) ) )
229 restsn2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ X e. ( 0 [,] 1 ) ) -> ( II |`t { X } ) = ~P { X } )
230 68 32 229 sylancr 
 |-  ( ph -> ( II |`t { X } ) = ~P { X } )
231 pwsn 
 |-  ~P { X } = { (/) , { X } }
232 indisconn 
 |-  { (/) , { X } } e. Conn
233 231 232 eqeltri 
 |-  ~P { X } e. Conn
234 230 233 eqeltrdi 
 |-  ( ph -> ( II |`t { X } ) e. Conn )
235 txconn 
 |-  ( ( ( II |`t { X } ) e. Conn /\ ( II |`t V ) e. Conn ) -> ( ( II |`t { X } ) tX ( II |`t V ) ) e. Conn )
236 234 14 235 syl2anc 
 |-  ( ph -> ( ( II |`t { X } ) tX ( II |`t V ) ) e. Conn )
237 228 236 eqeltrd 
 |-  ( ph -> ( ( II tX II ) |`t ( { X } X. V ) ) e. Conn )
238 1 2 3 4 5 6 7 cvmlift2lem6 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( K |` ( { X } X. ( 0 [,] 1 ) ) ) e. ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) Cn C ) )
239 32 238 mpdan 
 |-  ( ph -> ( K |` ( { X } X. ( 0 [,] 1 ) ) ) e. ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) Cn C ) )
240 xpss2 
 |-  ( V C_ ( 0 [,] 1 ) -> ( { X } X. V ) C_ ( { X } X. ( 0 [,] 1 ) ) )
241 12 34 240 3syl 
 |-  ( ph -> ( { X } X. V ) C_ ( { X } X. ( 0 [,] 1 ) ) )
242 32 snssd 
 |-  ( ph -> { X } C_ ( 0 [,] 1 ) )
243 xpss1 
 |-  ( { X } C_ ( 0 [,] 1 ) -> ( { X } X. ( 0 [,] 1 ) ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
244 242 243 syl 
 |-  ( ph -> ( { X } X. ( 0 [,] 1 ) ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
245 23 restuni 
 |-  ( ( ( II tX II ) e. Top /\ ( { X } X. ( 0 [,] 1 ) ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( { X } X. ( 0 [,] 1 ) ) = U. ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) )
246 27 244 245 sylancr 
 |-  ( ph -> ( { X } X. ( 0 [,] 1 ) ) = U. ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) )
247 241 246 sseqtrd 
 |-  ( ph -> ( { X } X. V ) C_ U. ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) )
248 eqid 
 |-  U. ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) = U. ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) )
249 248 cnrest 
 |-  ( ( ( K |` ( { X } X. ( 0 [,] 1 ) ) ) e. ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) Cn C ) /\ ( { X } X. V ) C_ U. ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) ) -> ( ( K |` ( { X } X. ( 0 [,] 1 ) ) ) |` ( { X } X. V ) ) e. ( ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) |`t ( { X } X. V ) ) Cn C ) )
250 239 247 249 syl2anc 
 |-  ( ph -> ( ( K |` ( { X } X. ( 0 [,] 1 ) ) ) |` ( { X } X. V ) ) e. ( ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) |`t ( { X } X. V ) ) Cn C ) )
251 241 resabs1d 
 |-  ( ph -> ( ( K |` ( { X } X. ( 0 [,] 1 ) ) ) |` ( { X } X. V ) ) = ( K |` ( { X } X. V ) ) )
252 225 97 xpex 
 |-  ( { X } X. ( 0 [,] 1 ) ) e. _V
253 252 a1i 
 |-  ( ph -> ( { X } X. ( 0 [,] 1 ) ) e. _V )
254 restabs 
 |-  ( ( ( II tX II ) e. Top /\ ( { X } X. V ) C_ ( { X } X. ( 0 [,] 1 ) ) /\ ( { X } X. ( 0 [,] 1 ) ) e. _V ) -> ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) |`t ( { X } X. V ) ) = ( ( II tX II ) |`t ( { X } X. V ) ) )
255 28 241 253 254 syl3anc 
 |-  ( ph -> ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) |`t ( { X } X. V ) ) = ( ( II tX II ) |`t ( { X } X. V ) ) )
256 255 oveq1d 
 |-  ( ph -> ( ( ( ( II tX II ) |`t ( { X } X. ( 0 [,] 1 ) ) ) |`t ( { X } X. V ) ) Cn C ) = ( ( ( II tX II ) |`t ( { X } X. V ) ) Cn C ) )
257 250 251 256 3eltr3d 
 |-  ( ph -> ( K |` ( { X } X. V ) ) e. ( ( ( II tX II ) |`t ( { X } X. V ) ) Cn C ) )
258 df-ima 
 |-  ( K " ( { X } X. V ) ) = ran ( K |` ( { X } X. V ) )
259 15 snssd 
 |-  ( ph -> { X } C_ U )
260 xpss1 
 |-  ( { X } C_ U -> ( { X } X. V ) C_ ( U X. V ) )
261 imass2 
 |-  ( ( { X } X. V ) C_ ( U X. V ) -> ( K " ( { X } X. V ) ) C_ ( K " ( U X. V ) ) )
262 259 260 261 3syl 
 |-  ( ph -> ( K " ( { X } X. V ) ) C_ ( K " ( U X. V ) ) )
263 262 127 sstrd 
 |-  ( ph -> ( K " ( { X } X. V ) ) C_ ( `' F " M ) )
264 258 263 eqsstrrid 
 |-  ( ph -> ran ( K |` ( { X } X. V ) ) C_ ( `' F " M ) )
265 cnrest2 
 |-  ( ( C e. ( TopOn ` B ) /\ ran ( K |` ( { X } X. V ) ) C_ ( `' F " M ) /\ ( `' F " M ) C_ B ) -> ( ( K |` ( { X } X. V ) ) e. ( ( ( II tX II ) |`t ( { X } X. V ) ) Cn C ) <-> ( K |` ( { X } X. V ) ) e. ( ( ( II tX II ) |`t ( { X } X. V ) ) Cn ( C |`t ( `' F " M ) ) ) ) )
266 196 264 138 265 syl3anc 
 |-  ( ph -> ( ( K |` ( { X } X. V ) ) e. ( ( ( II tX II ) |`t ( { X } X. V ) ) Cn C ) <-> ( K |` ( { X } X. V ) ) e. ( ( ( II tX II ) |`t ( { X } X. V ) ) Cn ( C |`t ( `' F " M ) ) ) ) )
267 257 266 mpbid 
 |-  ( ph -> ( K |` ( { X } X. V ) ) e. ( ( ( II tX II ) |`t ( { X } X. V ) ) Cn ( C |`t ( `' F " M ) ) ) )
268 opelxpi 
 |-  ( ( X e. { X } /\ Y e. V ) -> <. X , Y >. e. ( { X } X. V ) )
269 219 16 268 syl2anc 
 |-  ( ph -> <. X , Y >. e. ( { X } X. V ) )
270 259 260 syl 
 |-  ( ph -> ( { X } X. V ) C_ ( U X. V ) )
271 270 55 sstrd 
 |-  ( ph -> ( { X } X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
272 23 restuni 
 |-  ( ( ( II tX II ) e. Top /\ ( { X } X. V ) C_ ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) -> ( { X } X. V ) = U. ( ( II tX II ) |`t ( { X } X. V ) ) )
273 27 271 272 sylancr 
 |-  ( ph -> ( { X } X. V ) = U. ( ( II tX II ) |`t ( { X } X. V ) ) )
274 269 273 eleqtrd 
 |-  ( ph -> <. X , Y >. e. U. ( ( II tX II ) |`t ( { X } X. V ) ) )
275 df-ov 
 |-  ( X ( K |` ( { X } X. V ) ) Y ) = ( ( K |` ( { X } X. V ) ) ` <. X , Y >. )
276 ovres 
 |-  ( ( X e. { X } /\ Y e. V ) -> ( X ( K |` ( { X } X. V ) ) Y ) = ( X K Y ) )
277 219 16 276 syl2anc 
 |-  ( ph -> ( X ( K |` ( { X } X. V ) ) Y ) = ( X K Y ) )
278 275 277 eqtr3id 
 |-  ( ph -> ( ( K |` ( { X } X. V ) ) ` <. X , Y >. ) = ( X K Y ) )
279 50 simprd 
 |-  ( ph -> ( X K Y ) e. W )
280 278 279 eqeltrd 
 |-  ( ph -> ( ( K |` ( { X } X. V ) ) ` <. X , Y >. ) e. W )
281 224 237 267 158 161 274 280 conncn 
 |-  ( ph -> ( K |` ( { X } X. V ) ) : U. ( ( II tX II ) |`t ( { X } X. V ) ) --> W )
282 273 feq2d 
 |-  ( ph -> ( ( K |` ( { X } X. V ) ) : ( { X } X. V ) --> W <-> ( K |` ( { X } X. V ) ) : U. ( ( II tX II ) |`t ( { X } X. V ) ) --> W ) )
283 281 282 mpbird 
 |-  ( ph -> ( K |` ( { X } X. V ) ) : ( { X } X. V ) --> W )
284 283 219 18 fovrnd 
 |-  ( ph -> ( X ( K |` ( { X } X. V ) ) Z ) e. W )
285 223 284 eqeltrd 
 |-  ( ph -> ( ( K |` ( U X. { Z } ) ) ` <. X , Z >. ) e. W )
286 180 195 206 158 161 214 285 conncn 
 |-  ( ph -> ( K |` ( U X. { Z } ) ) : U. ( ( II tX II ) |`t ( U X. { Z } ) ) --> W )
287 213 feq2d 
 |-  ( ph -> ( ( K |` ( U X. { Z } ) ) : ( U X. { Z } ) --> W <-> ( K |` ( U X. { Z } ) ) : U. ( ( II tX II ) |`t ( U X. { Z } ) ) --> W ) )
288 286 287 mpbird 
 |-  ( ph -> ( K |` ( U X. { Z } ) ) : ( U X. { Z } ) --> W )
289 288 adantr 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( K |` ( U X. { Z } ) ) : ( U X. { Z } ) --> W )
290 289 110 175 fovrnd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( m ( K |` ( U X. { Z } ) ) Z ) e. W )
291 179 290 eqeltrd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( K |` ( { m } X. V ) ) ` <. m , Z >. ) e. W )
292 61 80 142 159 162 169 291 conncn 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( K |` ( { m } X. V ) ) : U. ( ( II tX II ) |`t ( { m } X. V ) ) --> W )
293 168 feq2d 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( ( K |` ( { m } X. V ) ) : ( { m } X. V ) --> W <-> ( K |` ( { m } X. V ) ) : U. ( ( II tX II ) |`t ( { m } X. V ) ) --> W ) )
294 292 293 mpbird 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( K |` ( { m } X. V ) ) : ( { m } X. V ) --> W )
295 294 57 58 fovrnd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( m ( K |` ( { m } X. V ) ) n ) e. W )
296 60 295 eqeltrrd 
 |-  ( ( ph /\ ( m e. U /\ n e. V ) ) -> ( m K n ) e. W )
297 296 ralrimivva 
 |-  ( ph -> A. m e. U A. n e. V ( m K n ) e. W )
298 funimassov 
 |-  ( ( Fun K /\ ( U X. V ) C_ dom K ) -> ( ( K " ( U X. V ) ) C_ W <-> A. m e. U A. n e. V ( m K n ) e. W ) )
299 122 124 298 syl2anc 
 |-  ( ph -> ( ( K " ( U X. V ) ) C_ W <-> A. m e. U A. n e. V ( m K n ) e. W ) )
300 297 299 mpbird 
 |-  ( ph -> ( K " ( U X. V ) ) C_ W )
301 1 23 8 2 24 26 28 38 10 53 55 300 cvmlift2lem9a 
 |-  ( ph -> ( K |` ( U X. V ) ) e. ( ( ( II tX II ) |`t ( U X. V ) ) Cn C ) )