Metamath Proof Explorer

Theorem cvmlift3lem7

Description: Lemma for cvmlift3 . (Contributed by Mario Carneiro, 9-Jul-2015)

Ref Expression
Hypotheses cvmlift3.b 
|- B = U. C
cvmlift3.y 
|- Y = U. K
cvmlift3.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmlift3.k 
|- ( ph -> K e. SConn )
cvmlift3.l 
|- ( ph -> K e. N-Locally PConn )
cvmlift3.o 
|- ( ph -> O e. Y )
cvmlift3.g 
|- ( ph -> G e. ( K Cn J ) )
cvmlift3.p 
|- ( ph -> P e. B )
cvmlift3.e 
|- ( ph -> ( F ` P ) = ( G ` O ) )
cvmlift3.h 
|- H = ( x e. Y |-> ( iota_ z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
cvmlift3lem7.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 ) ) ) ) } )
cvmlift3lem7.1 
|- ( ph -> ( G ` X ) e. A )
cvmlift3lem7.2 
|- ( ph -> T e. ( S ` A ) )
cvmlift3lem7.3 
|- ( ph -> M C_ ( `' G " A ) )
cvmlift3lem7.w 
|- W = ( iota_ b e. T ( H ` X ) e. b )
cvmlift3lem7.7 
|- ( ph -> ( K |`t M ) e. PConn )
cvmlift3lem7.4 
|- ( ph -> V e. K )
cvmlift3lem7.5 
|- ( ph -> V C_ M )
cvmlift3lem7.6 
|- ( ph -> X e. V )
Assertion cvmlift3lem7 
|- ( ph -> H e. ( ( K CnP C ) ` X ) )

Proof

Step Hyp Ref Expression
1 cvmlift3.b 
 |-  B = U. C
2 cvmlift3.y 
 |-  Y = U. K
3 cvmlift3.f 
 |-  ( ph -> F e. ( C CovMap J ) )
4 cvmlift3.k 
 |-  ( ph -> K e. SConn )
5 cvmlift3.l 
 |-  ( ph -> K e. N-Locally PConn )
6 cvmlift3.o 
 |-  ( ph -> O e. Y )
7 cvmlift3.g 
 |-  ( ph -> G e. ( K Cn J ) )
8 cvmlift3.p 
 |-  ( ph -> P e. B )
9 cvmlift3.e 
 |-  ( ph -> ( F ` P ) = ( G ` O ) )
10 cvmlift3.h 
 |-  H = ( x e. Y |-> ( iota_ z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
11 cvmlift3lem7.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 ) ) ) ) } )
12 cvmlift3lem7.1 
 |-  ( ph -> ( G ` X ) e. A )
13 cvmlift3lem7.2 
 |-  ( ph -> T e. ( S ` A ) )
14 cvmlift3lem7.3 
 |-  ( ph -> M C_ ( `' G " A ) )
15 cvmlift3lem7.w 
 |-  W = ( iota_ b e. T ( H ` X ) e. b )
16 cvmlift3lem7.7 
 |-  ( ph -> ( K |`t M ) e. PConn )
17 cvmlift3lem7.4 
 |-  ( ph -> V e. K )
18 cvmlift3lem7.5 
 |-  ( ph -> V C_ M )
19 cvmlift3lem7.6 
 |-  ( ph -> X e. V )
20 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 
 |-  ( ph -> H : Y --> B )
21 1 2 3 4 5 6 7 8 9 10 cvmlift3lem5 
 |-  ( ph -> ( F o. H ) = G )
22 21 7 eqeltrd 
 |-  ( ph -> ( F o. H ) e. ( K Cn J ) )
23 sconntop 
 |-  ( K e. SConn -> K e. Top )
24 4 23 syl 
 |-  ( ph -> K e. Top )
25 cnvimass 
 |-  ( `' G " A ) C_ dom G
26 eqid 
 |-  U. J = U. J
27 2 26 cnf 
 |-  ( G e. ( K Cn J ) -> G : Y --> U. J )
28 fdm 
 |-  ( G : Y --> U. J -> dom G = Y )
29 7 27 28 3syl 
 |-  ( ph -> dom G = Y )
30 25 29 sseqtrid 
 |-  ( ph -> ( `' G " A ) C_ Y )
31 14 30 sstrd 
 |-  ( ph -> M C_ Y )
32 18 19 sseldd 
 |-  ( ph -> X e. M )
33 31 32 sseldd 
 |-  ( ph -> X e. Y )
34 20 33 ffvelcdmd 
 |-  ( ph -> ( H ` X ) e. B )
35 fvco3 
 |-  ( ( H : Y --> B /\ X e. Y ) -> ( ( F o. H ) ` X ) = ( F ` ( H ` X ) ) )
36 20 33 35 syl2anc 
 |-  ( ph -> ( ( F o. H ) ` X ) = ( F ` ( H ` X ) ) )
37 21 fveq1d 
 |-  ( ph -> ( ( F o. H ) ` X ) = ( G ` X ) )
38 36 37 eqtr3d 
 |-  ( ph -> ( F ` ( H ` X ) ) = ( G ` X ) )
39 38 12 eqeltrd 
 |-  ( ph -> ( F ` ( H ` X ) ) e. A )
40 11 1 15 cvmsiota 
 |-  ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` A ) /\ ( H ` X ) e. B /\ ( F ` ( H ` X ) ) e. A ) ) -> ( W e. T /\ ( H ` X ) e. W ) )
41 3 13 34 39 40 syl13anc 
 |-  ( ph -> ( W e. T /\ ( H ` X ) e. W ) )
42 eqid 
 |-  ( H ` X ) = ( H ` X )
43 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 
 |-  ( ( ph /\ X e. Y ) -> ( ( H ` X ) = ( H ` X ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) ) )
44 42 43 mpbii 
 |-  ( ( ph /\ X e. Y ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) )
45 33 44 mpdan 
 |-  ( ph -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) )
46 45 adantr 
 |-  ( ( ph /\ y e. M ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) )
47 fveq1 
 |-  ( f = h -> ( f ` 0 ) = ( h ` 0 ) )
48 47 eqeq1d 
 |-  ( f = h -> ( ( f ` 0 ) = O <-> ( h ` 0 ) = O ) )
49 fveq1 
 |-  ( f = h -> ( f ` 1 ) = ( h ` 1 ) )
50 49 eqeq1d 
 |-  ( f = h -> ( ( f ` 1 ) = X <-> ( h ` 1 ) = X ) )
51 coeq2 
 |-  ( f = h -> ( G o. f ) = ( G o. h ) )
52 51 eqeq2d 
 |-  ( f = h -> ( ( F o. g ) = ( G o. f ) <-> ( F o. g ) = ( G o. h ) ) )
53 52 anbi1d 
 |-  ( f = h -> ( ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) <-> ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) )
54 53 riotabidv 
 |-  ( f = h -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) )
55 coeq2 
 |-  ( a = g -> ( F o. a ) = ( F o. g ) )
56 55 eqeq1d 
 |-  ( a = g -> ( ( F o. a ) = ( G o. h ) <-> ( F o. g ) = ( G o. h ) ) )
57 fveq1 
 |-  ( a = g -> ( a ` 0 ) = ( g ` 0 ) )
58 57 eqeq1d 
 |-  ( a = g -> ( ( a ` 0 ) = P <-> ( g ` 0 ) = P ) )
59 56 58 anbi12d 
 |-  ( a = g -> ( ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) <-> ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) )
60 59 cbvriotavw 
 |-  ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) )
61 54 60 eqtr4di 
 |-  ( f = h -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) = ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) )
62 61 fveq1d 
 |-  ( f = h -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) )
63 62 eqeq1d 
 |-  ( f = h -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` X ) <-> ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) )
64 48 50 63 3anbi123d 
 |-  ( f = h -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) <-> ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) ) )
65 64 cbvrexvw 
 |-  ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) <-> E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) )
66 46 65 sylib 
 |-  ( ( ph /\ y e. M ) -> E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) )
67 16 adantr 
 |-  ( ( ph /\ y e. M ) -> ( K |`t M ) e. PConn )
68 2 restuni 
 |-  ( ( K e. Top /\ M C_ Y ) -> M = U. ( K |`t M ) )
69 24 31 68 syl2anc 
 |-  ( ph -> M = U. ( K |`t M ) )
70 32 69 eleqtrd 
 |-  ( ph -> X e. U. ( K |`t M ) )
71 70 adantr 
 |-  ( ( ph /\ y e. M ) -> X e. U. ( K |`t M ) )
72 69 eleq2d 
 |-  ( ph -> ( y e. M <-> y e. U. ( K |`t M ) ) )
73 72 biimpa 
 |-  ( ( ph /\ y e. M ) -> y e. U. ( K |`t M ) )
74 eqid 
 |-  U. ( K |`t M ) = U. ( K |`t M )
75 74 pconncn 
 |-  ( ( ( K |`t M ) e. PConn /\ X e. U. ( K |`t M ) /\ y e. U. ( K |`t M ) ) -> E. n e. ( II Cn ( K |`t M ) ) ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) )
76 67 71 73 75 syl3anc 
 |-  ( ( ph /\ y e. M ) -> E. n e. ( II Cn ( K |`t M ) ) ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) )
77 reeanv 
 |-  ( E. h e. ( II Cn K ) E. n e. ( II Cn ( K |`t M ) ) ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) <-> ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ E. n e. ( II Cn ( K |`t M ) ) ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) )
78 3 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> F e. ( C CovMap J ) )
79 4 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> K e. SConn )
80 5 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> K e. N-Locally PConn )
81 6 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> O e. Y )
82 7 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> G e. ( K Cn J ) )
83 8 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> P e. B )
84 9 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> ( F ` P ) = ( G ` O ) )
85 12 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> ( G ` X ) e. A )
86 13 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> T e. ( S ` A ) )
87 14 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> M C_ ( `' G " A ) )
88 32 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> X e. M )
89 simpllr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> y e. M )
90 simplrl 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> h e. ( II Cn K ) )
91 simprl 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) )
92 simplrr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> n e. ( II Cn ( K |`t M ) ) )
93 simprr 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) )
94 55 eqeq1d 
 |-  ( a = g -> ( ( F o. a ) = ( G o. n ) <-> ( F o. g ) = ( G o. n ) ) )
95 57 eqeq1d 
 |-  ( a = g -> ( ( a ` 0 ) = ( H ` X ) <-> ( g ` 0 ) = ( H ` X ) ) )
96 94 95 anbi12d 
 |-  ( a = g -> ( ( ( F o. a ) = ( G o. n ) /\ ( a ` 0 ) = ( H ` X ) ) <-> ( ( F o. g ) = ( G o. n ) /\ ( g ` 0 ) = ( H ` X ) ) ) )
97 96 cbvriotavw 
 |-  ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. n ) /\ ( a ` 0 ) = ( H ` X ) ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. n ) /\ ( g ` 0 ) = ( H ` X ) ) )
98 1 2 78 79 80 81 82 83 84 10 11 85 86 87 15 88 89 90 60 91 92 93 97 cvmlift3lem6 
 |-  ( ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) /\ ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) ) -> ( H ` y ) e. W )
99 98 ex 
 |-  ( ( ( ph /\ y e. M ) /\ ( h e. ( II Cn K ) /\ n e. ( II Cn ( K |`t M ) ) ) ) -> ( ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) -> ( H ` y ) e. W ) )
100 99 rexlimdvva 
 |-  ( ( ph /\ y e. M ) -> ( E. h e. ( II Cn K ) E. n e. ( II Cn ( K |`t M ) ) ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) -> ( H ` y ) e. W ) )
101 77 100 biimtrrid 
 |-  ( ( ph /\ y e. M ) -> ( ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ a e. ( II Cn C ) ( ( F o. a ) = ( G o. h ) /\ ( a ` 0 ) = P ) ) ` 1 ) = ( H ` X ) ) /\ E. n e. ( II Cn ( K |`t M ) ) ( ( n ` 0 ) = X /\ ( n ` 1 ) = y ) ) -> ( H ` y ) e. W ) )
102 66 76 101 mp2and 
 |-  ( ( ph /\ y e. M ) -> ( H ` y ) e. W )
103 102 ralrimiva 
 |-  ( ph -> A. y e. M ( H ` y ) e. W )
104 20 ffund 
 |-  ( ph -> Fun H )
105 20 fdmd 
 |-  ( ph -> dom H = Y )
106 31 105 sseqtrrd 
 |-  ( ph -> M C_ dom H )
107 funimass4 
 |-  ( ( Fun H /\ M C_ dom H ) -> ( ( H " M ) C_ W <-> A. y e. M ( H ` y ) e. W ) )
108 104 106 107 syl2anc 
 |-  ( ph -> ( ( H " M ) C_ W <-> A. y e. M ( H ` y ) e. W ) )
109 103 108 mpbird 
 |-  ( ph -> ( H " M ) C_ W )
110 1 2 11 3 20 22 24 33 13 41 31 109 cvmlift2lem9a 
 |-  ( ph -> ( H |` M ) e. ( ( K |`t M ) Cn C ) )
111 74 cncnpi 
 |-  ( ( ( H |` M ) e. ( ( K |`t M ) Cn C ) /\ X e. U. ( K |`t M ) ) -> ( H |` M ) e. ( ( ( K |`t M ) CnP C ) ` X ) )
112 110 70 111 syl2anc 
 |-  ( ph -> ( H |` M ) e. ( ( ( K |`t M ) CnP C ) ` X ) )
113 2 ssntr 
 |-  ( ( ( K e. Top /\ M C_ Y ) /\ ( V e. K /\ V C_ M ) ) -> V C_ ( ( int ` K ) ` M ) )
114 24 31 17 18 113 syl22anc 
 |-  ( ph -> V C_ ( ( int ` K ) ` M ) )
115 114 19 sseldd 
 |-  ( ph -> X e. ( ( int ` K ) ` M ) )
116 2 1 cnprest 
 |-  ( ( ( K e. Top /\ M C_ Y ) /\ ( X e. ( ( int ` K ) ` M ) /\ H : Y --> B ) ) -> ( H e. ( ( K CnP C ) ` X ) <-> ( H |` M ) e. ( ( ( K |`t M ) CnP C ) ` X ) ) )
117 24 31 115 20 116 syl22anc 
 |-  ( ph -> ( H e. ( ( K CnP C ) ` X ) <-> ( H |` M ) e. ( ( ( K |`t M ) CnP C ) ` X ) ) )
118 112 117 mpbird 
 |-  ( ph -> H e. ( ( K CnP C ) ` X ) )