Metamath Proof Explorer

Theorem cvmlift3lem6

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 )
cvmlift3lem6.x 
|- ( ph -> X e. M )
cvmlift3lem6.z 
|- ( ph -> Z e. M )
cvmlift3lem6.q 
|- ( ph -> Q e. ( II Cn K ) )
cvmlift3lem6.r 
|- R = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. Q ) /\ ( g ` 0 ) = P ) )
cvmlift3lem6.1 
|- ( ph -> ( ( Q ` 0 ) = O /\ ( Q ` 1 ) = X /\ ( R ` 1 ) = ( H ` X ) ) )
cvmlift3lem6.n 
|- ( ph -> N e. ( II Cn ( K |`t M ) ) )
cvmlift3lem6.2 
|- ( ph -> ( ( N ` 0 ) = X /\ ( N ` 1 ) = Z ) )
cvmlift3lem6.i 
|- I = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = ( H ` X ) ) )
Assertion cvmlift3lem6 
|- ( ph -> ( H ` Z ) e. W )

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 cvmlift3lem6.x 
 |-  ( ph -> X e. M )
17 cvmlift3lem6.z 
 |-  ( ph -> Z e. M )
18 cvmlift3lem6.q 
 |-  ( ph -> Q e. ( II Cn K ) )
19 cvmlift3lem6.r 
 |-  R = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. Q ) /\ ( g ` 0 ) = P ) )
20 cvmlift3lem6.1 
 |-  ( ph -> ( ( Q ` 0 ) = O /\ ( Q ` 1 ) = X /\ ( R ` 1 ) = ( H ` X ) ) )
21 cvmlift3lem6.n 
 |-  ( ph -> N e. ( II Cn ( K |`t M ) ) )
22 cvmlift3lem6.2 
 |-  ( ph -> ( ( N ` 0 ) = X /\ ( N ` 1 ) = Z ) )
23 cvmlift3lem6.i 
 |-  I = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = ( H ` X ) ) )
24 sconntop 
 |-  ( K e. SConn -> K e. Top )
25 4 24 syl 
 |-  ( ph -> K e. Top )
26 cnrest2r 
 |-  ( K e. Top -> ( II Cn ( K |`t M ) ) C_ ( II Cn K ) )
27 25 26 syl 
 |-  ( ph -> ( II Cn ( K |`t M ) ) C_ ( II Cn K ) )
28 27 21 sseldd 
 |-  ( ph -> N e. ( II Cn K ) )
29 20 simp2d 
 |-  ( ph -> ( Q ` 1 ) = X )
30 22 simpld 
 |-  ( ph -> ( N ` 0 ) = X )
31 29 30 eqtr4d 
 |-  ( ph -> ( Q ` 1 ) = ( N ` 0 ) )
32 18 28 31 pcocn 
 |-  ( ph -> ( Q ( *p ` K ) N ) e. ( II Cn K ) )
33 18 28 pco0 
 |-  ( ph -> ( ( Q ( *p ` K ) N ) ` 0 ) = ( Q ` 0 ) )
34 20 simp1d 
 |-  ( ph -> ( Q ` 0 ) = O )
35 33 34 eqtrd 
 |-  ( ph -> ( ( Q ( *p ` K ) N ) ` 0 ) = O )
36 18 28 pco1 
 |-  ( ph -> ( ( Q ( *p ` K ) N ) ` 1 ) = ( N ` 1 ) )
37 22 simprd 
 |-  ( ph -> ( N ` 1 ) = Z )
38 36 37 eqtrd 
 |-  ( ph -> ( ( Q ( *p ` K ) N ) ` 1 ) = Z )
39 cnco 
 |-  ( ( Q e. ( II Cn K ) /\ G e. ( K Cn J ) ) -> ( G o. Q ) e. ( II Cn J ) )
40 18 7 39 syl2anc 
 |-  ( ph -> ( G o. Q ) e. ( II Cn J ) )
41 34 fveq2d 
 |-  ( ph -> ( G ` ( Q ` 0 ) ) = ( G ` O ) )
42 iiuni 
 |-  ( 0 [,] 1 ) = U. II
43 42 2 cnf 
 |-  ( Q e. ( II Cn K ) -> Q : ( 0 [,] 1 ) --> Y )
44 18 43 syl 
 |-  ( ph -> Q : ( 0 [,] 1 ) --> Y )
45 0elunit 
 |-  0 e. ( 0 [,] 1 )
46 fvco3 
 |-  ( ( Q : ( 0 [,] 1 ) --> Y /\ 0 e. ( 0 [,] 1 ) ) -> ( ( G o. Q ) ` 0 ) = ( G ` ( Q ` 0 ) ) )
47 44 45 46 sylancl 
 |-  ( ph -> ( ( G o. Q ) ` 0 ) = ( G ` ( Q ` 0 ) ) )
48 41 47 9 3eqtr4rd 
 |-  ( ph -> ( F ` P ) = ( ( G o. Q ) ` 0 ) )
49 1 19 3 40 8 48 cvmliftiota 
 |-  ( ph -> ( R e. ( II Cn C ) /\ ( F o. R ) = ( G o. Q ) /\ ( R ` 0 ) = P ) )
50 49 simp2d 
 |-  ( ph -> ( F o. R ) = ( G o. Q ) )
51 cnco 
 |-  ( ( N e. ( II Cn K ) /\ G e. ( K Cn J ) ) -> ( G o. N ) e. ( II Cn J ) )
52 28 7 51 syl2anc 
 |-  ( ph -> ( G o. N ) e. ( II Cn J ) )
53 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 
 |-  ( ph -> H : Y --> B )
54 cnvimass 
 |-  ( `' G " A ) C_ dom G
55 eqid 
 |-  U. J = U. J
56 2 55 cnf 
 |-  ( G e. ( K Cn J ) -> G : Y --> U. J )
57 7 56 syl 
 |-  ( ph -> G : Y --> U. J )
58 54 57 fssdm 
 |-  ( ph -> ( `' G " A ) C_ Y )
59 14 58 sstrd 
 |-  ( ph -> M C_ Y )
60 59 16 sseldd 
 |-  ( ph -> X e. Y )
61 53 60 ffvelrnd 
 |-  ( ph -> ( H ` X ) e. B )
62 30 fveq2d 
 |-  ( ph -> ( G ` ( N ` 0 ) ) = ( G ` X ) )
63 42 2 cnf 
 |-  ( N e. ( II Cn K ) -> N : ( 0 [,] 1 ) --> Y )
64 28 63 syl 
 |-  ( ph -> N : ( 0 [,] 1 ) --> Y )
65 fvco3 
 |-  ( ( N : ( 0 [,] 1 ) --> Y /\ 0 e. ( 0 [,] 1 ) ) -> ( ( G o. N ) ` 0 ) = ( G ` ( N ` 0 ) ) )
66 64 45 65 sylancl 
 |-  ( ph -> ( ( G o. N ) ` 0 ) = ( G ` ( N ` 0 ) ) )
67 fvco3 
 |-  ( ( H : Y --> B /\ X e. Y ) -> ( ( F o. H ) ` X ) = ( F ` ( H ` X ) ) )
68 53 60 67 syl2anc 
 |-  ( ph -> ( ( F o. H ) ` X ) = ( F ` ( H ` X ) ) )
69 1 2 3 4 5 6 7 8 9 10 cvmlift3lem5 
 |-  ( ph -> ( F o. H ) = G )
70 69 fveq1d 
 |-  ( ph -> ( ( F o. H ) ` X ) = ( G ` X ) )
71 68 70 eqtr3d 
 |-  ( ph -> ( F ` ( H ` X ) ) = ( G ` X ) )
72 62 66 71 3eqtr4rd 
 |-  ( ph -> ( F ` ( H ` X ) ) = ( ( G o. N ) ` 0 ) )
73 1 23 3 52 61 72 cvmliftiota 
 |-  ( ph -> ( I e. ( II Cn C ) /\ ( F o. I ) = ( G o. N ) /\ ( I ` 0 ) = ( H ` X ) ) )
74 73 simp2d 
 |-  ( ph -> ( F o. I ) = ( G o. N ) )
75 50 74 oveq12d 
 |-  ( ph -> ( ( F o. R ) ( *p ` J ) ( F o. I ) ) = ( ( G o. Q ) ( *p ` J ) ( G o. N ) ) )
76 49 simp1d 
 |-  ( ph -> R e. ( II Cn C ) )
77 73 simp1d 
 |-  ( ph -> I e. ( II Cn C ) )
78 20 simp3d 
 |-  ( ph -> ( R ` 1 ) = ( H ` X ) )
79 73 simp3d 
 |-  ( ph -> ( I ` 0 ) = ( H ` X ) )
80 78 79 eqtr4d 
 |-  ( ph -> ( R ` 1 ) = ( I ` 0 ) )
81 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
82 3 81 syl 
 |-  ( ph -> F e. ( C Cn J ) )
83 76 77 80 82 copco 
 |-  ( ph -> ( F o. ( R ( *p ` C ) I ) ) = ( ( F o. R ) ( *p ` J ) ( F o. I ) ) )
84 18 28 31 7 copco 
 |-  ( ph -> ( G o. ( Q ( *p ` K ) N ) ) = ( ( G o. Q ) ( *p ` J ) ( G o. N ) ) )
85 75 83 84 3eqtr4d 
 |-  ( ph -> ( F o. ( R ( *p ` C ) I ) ) = ( G o. ( Q ( *p ` K ) N ) ) )
86 76 77 pco0 
 |-  ( ph -> ( ( R ( *p ` C ) I ) ` 0 ) = ( R ` 0 ) )
87 49 simp3d 
 |-  ( ph -> ( R ` 0 ) = P )
88 86 87 eqtrd 
 |-  ( ph -> ( ( R ( *p ` C ) I ) ` 0 ) = P )
89 76 77 80 pcocn 
 |-  ( ph -> ( R ( *p ` C ) I ) e. ( II Cn C ) )
90 cnco 
 |-  ( ( ( Q ( *p ` K ) N ) e. ( II Cn K ) /\ G e. ( K Cn J ) ) -> ( G o. ( Q ( *p ` K ) N ) ) e. ( II Cn J ) )
91 32 7 90 syl2anc 
 |-  ( ph -> ( G o. ( Q ( *p ` K ) N ) ) e. ( II Cn J ) )
92 35 fveq2d 
 |-  ( ph -> ( G ` ( ( Q ( *p ` K ) N ) ` 0 ) ) = ( G ` O ) )
93 42 2 cnf 
 |-  ( ( Q ( *p ` K ) N ) e. ( II Cn K ) -> ( Q ( *p ` K ) N ) : ( 0 [,] 1 ) --> Y )
94 32 93 syl 
 |-  ( ph -> ( Q ( *p ` K ) N ) : ( 0 [,] 1 ) --> Y )
95 fvco3 
 |-  ( ( ( Q ( *p ` K ) N ) : ( 0 [,] 1 ) --> Y /\ 0 e. ( 0 [,] 1 ) ) -> ( ( G o. ( Q ( *p ` K ) N ) ) ` 0 ) = ( G ` ( ( Q ( *p ` K ) N ) ` 0 ) ) )
96 94 45 95 sylancl 
 |-  ( ph -> ( ( G o. ( Q ( *p ` K ) N ) ) ` 0 ) = ( G ` ( ( Q ( *p ` K ) N ) ` 0 ) ) )
97 92 96 9 3eqtr4rd 
 |-  ( ph -> ( F ` P ) = ( ( G o. ( Q ( *p ` K ) N ) ) ` 0 ) )
98 1 cvmlift 
 |-  ( ( ( F e. ( C CovMap J ) /\ ( G o. ( Q ( *p ` K ) N ) ) e. ( II Cn J ) ) /\ ( P e. B /\ ( F ` P ) = ( ( G o. ( Q ( *p ` K ) N ) ) ` 0 ) ) ) -> E! g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) )
99 3 91 8 97 98 syl22anc 
 |-  ( ph -> E! g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) )
100 coeq2 
 |-  ( g = ( R ( *p ` C ) I ) -> ( F o. g ) = ( F o. ( R ( *p ` C ) I ) ) )
101 100 eqeq1d 
 |-  ( g = ( R ( *p ` C ) I ) -> ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) <-> ( F o. ( R ( *p ` C ) I ) ) = ( G o. ( Q ( *p ` K ) N ) ) ) )
102 fveq1 
 |-  ( g = ( R ( *p ` C ) I ) -> ( g ` 0 ) = ( ( R ( *p ` C ) I ) ` 0 ) )
103 102 eqeq1d 
 |-  ( g = ( R ( *p ` C ) I ) -> ( ( g ` 0 ) = P <-> ( ( R ( *p ` C ) I ) ` 0 ) = P ) )
104 101 103 anbi12d 
 |-  ( g = ( R ( *p ` C ) I ) -> ( ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) <-> ( ( F o. ( R ( *p ` C ) I ) ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( ( R ( *p ` C ) I ) ` 0 ) = P ) ) )
105 104 riota2 
 |-  ( ( ( R ( *p ` C ) I ) e. ( II Cn C ) /\ E! g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) -> ( ( ( F o. ( R ( *p ` C ) I ) ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( ( R ( *p ` C ) I ) ` 0 ) = P ) <-> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) = ( R ( *p ` C ) I ) ) )
106 89 99 105 syl2anc 
 |-  ( ph -> ( ( ( F o. ( R ( *p ` C ) I ) ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( ( R ( *p ` C ) I ) ` 0 ) = P ) <-> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) = ( R ( *p ` C ) I ) ) )
107 85 88 106 mpbi2and 
 |-  ( ph -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) = ( R ( *p ` C ) I ) )
108 107 fveq1d 
 |-  ( ph -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( R ( *p ` C ) I ) ` 1 ) )
109 76 77 pco1 
 |-  ( ph -> ( ( R ( *p ` C ) I ) ` 1 ) = ( I ` 1 ) )
110 108 109 eqtrd 
 |-  ( ph -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) )
111 fveq1 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( f ` 0 ) = ( ( Q ( *p ` K ) N ) ` 0 ) )
112 111 eqeq1d 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( ( f ` 0 ) = O <-> ( ( Q ( *p ` K ) N ) ` 0 ) = O ) )
113 fveq1 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( f ` 1 ) = ( ( Q ( *p ` K ) N ) ` 1 ) )
114 113 eqeq1d 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( ( f ` 1 ) = Z <-> ( ( Q ( *p ` K ) N ) ` 1 ) = Z ) )
115 coeq2 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( G o. f ) = ( G o. ( Q ( *p ` K ) N ) ) )
116 115 eqeq2d 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( ( F o. g ) = ( G o. f ) <-> ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) ) )
117 116 anbi1d 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) <-> ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) )
118 117 riotabidv 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( 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. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) )
119 118 fveq1d 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) )
120 119 eqeq1d 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) <-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) ) )
121 112 114 120 3anbi123d 
 |-  ( f = ( Q ( *p ` K ) N ) -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = Z /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) ) <-> ( ( ( Q ( *p ` K ) N ) ` 0 ) = O /\ ( ( Q ( *p ` K ) N ) ` 1 ) = Z /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) ) ) )
122 121 rspcev 
 |-  ( ( ( Q ( *p ` K ) N ) e. ( II Cn K ) /\ ( ( ( Q ( *p ` K ) N ) ` 0 ) = O /\ ( ( Q ( *p ` K ) N ) ` 1 ) = Z /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( Q ( *p ` K ) N ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = Z /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) ) )
123 32 35 38 110 122 syl13anc 
 |-  ( ph -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = Z /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) ) )
124 59 17 sseldd 
 |-  ( ph -> Z e. Y )
125 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 
 |-  ( ( ph /\ Z e. Y ) -> ( ( H ` Z ) = ( I ` 1 ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = Z /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) ) ) )
126 124 125 mpdan 
 |-  ( ph -> ( ( H ` Z ) = ( I ` 1 ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = Z /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( I ` 1 ) ) ) )
127 123 126 mpbird 
 |-  ( ph -> ( H ` Z ) = ( I ` 1 ) )
128 iiconn 
 |-  II e. Conn
129 128 a1i 
 |-  ( ph -> II e. Conn )
130 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
131 3 130 syl 
 |-  ( ph -> C e. Top )
132 1 toptopon 
 |-  ( C e. Top <-> C e. ( TopOn ` B ) )
133 131 132 sylib 
 |-  ( ph -> C e. ( TopOn ` B ) )
134 74 rneqd 
 |-  ( ph -> ran ( F o. I ) = ran ( G o. N ) )
135 rnco2 
 |-  ran ( F o. I ) = ( F " ran I )
136 rnco2 
 |-  ran ( G o. N ) = ( G " ran N )
137 134 135 136 3eqtr3g 
 |-  ( ph -> ( F " ran I ) = ( G " ran N ) )
138 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
139 138 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
140 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
141 25 140 sylib 
 |-  ( ph -> K e. ( TopOn ` Y ) )
142 resttopon 
 |-  ( ( K e. ( TopOn ` Y ) /\ M C_ Y ) -> ( K |`t M ) e. ( TopOn ` M ) )
143 141 59 142 syl2anc 
 |-  ( ph -> ( K |`t M ) e. ( TopOn ` M ) )
144 cnf2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ ( K |`t M ) e. ( TopOn ` M ) /\ N e. ( II Cn ( K |`t M ) ) ) -> N : ( 0 [,] 1 ) --> M )
145 139 143 21 144 syl3anc 
 |-  ( ph -> N : ( 0 [,] 1 ) --> M )
146 145 frnd 
 |-  ( ph -> ran N C_ M )
147 146 14 sstrd 
 |-  ( ph -> ran N C_ ( `' G " A ) )
148 57 ffund 
 |-  ( ph -> Fun G )
149 147 54 sstrdi 
 |-  ( ph -> ran N C_ dom G )
150 funimass3 
 |-  ( ( Fun G /\ ran N C_ dom G ) -> ( ( G " ran N ) C_ A <-> ran N C_ ( `' G " A ) ) )
151 148 149 150 syl2anc 
 |-  ( ph -> ( ( G " ran N ) C_ A <-> ran N C_ ( `' G " A ) ) )
152 147 151 mpbird 
 |-  ( ph -> ( G " ran N ) C_ A )
153 137 152 eqsstrd 
 |-  ( ph -> ( F " ran I ) C_ A )
154 1 55 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> U. J )
155 82 154 syl 
 |-  ( ph -> F : B --> U. J )
156 155 ffund 
 |-  ( ph -> Fun F )
157 42 1 cnf 
 |-  ( I e. ( II Cn C ) -> I : ( 0 [,] 1 ) --> B )
158 77 157 syl 
 |-  ( ph -> I : ( 0 [,] 1 ) --> B )
159 158 frnd 
 |-  ( ph -> ran I C_ B )
160 155 fdmd 
 |-  ( ph -> dom F = B )
161 159 160 sseqtrrd 
 |-  ( ph -> ran I C_ dom F )
162 funimass3 
 |-  ( ( Fun F /\ ran I C_ dom F ) -> ( ( F " ran I ) C_ A <-> ran I C_ ( `' F " A ) ) )
163 156 161 162 syl2anc 
 |-  ( ph -> ( ( F " ran I ) C_ A <-> ran I C_ ( `' F " A ) ) )
164 153 163 mpbid 
 |-  ( ph -> ran I C_ ( `' F " A ) )
165 cnvimass 
 |-  ( `' F " A ) C_ dom F
166 165 155 fssdm 
 |-  ( ph -> ( `' F " A ) C_ B )
167 cnrest2 
 |-  ( ( C e. ( TopOn ` B ) /\ ran I C_ ( `' F " A ) /\ ( `' F " A ) C_ B ) -> ( I e. ( II Cn C ) <-> I e. ( II Cn ( C |`t ( `' F " A ) ) ) ) )
168 133 164 166 167 syl3anc 
 |-  ( ph -> ( I e. ( II Cn C ) <-> I e. ( II Cn ( C |`t ( `' F " A ) ) ) ) )
169 77 168 mpbid 
 |-  ( ph -> I e. ( II Cn ( C |`t ( `' F " A ) ) ) )
170 11 cvmsss 
 |-  ( T e. ( S ` A ) -> T C_ C )
171 13 170 syl 
 |-  ( ph -> T C_ C )
172 71 12 eqeltrd 
 |-  ( ph -> ( F ` ( H ` X ) ) e. A )
173 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 ) )
174 3 13 61 172 173 syl13anc 
 |-  ( ph -> ( W e. T /\ ( H ` X ) e. W ) )
175 174 simpld 
 |-  ( ph -> W e. T )
176 171 175 sseldd 
 |-  ( ph -> W e. C )
177 elssuni 
 |-  ( W e. T -> W C_ U. T )
178 175 177 syl 
 |-  ( ph -> W C_ U. T )
179 11 cvmsuni 
 |-  ( T e. ( S ` A ) -> U. T = ( `' F " A ) )
180 13 179 syl 
 |-  ( ph -> U. T = ( `' F " A ) )
181 178 180 sseqtrd 
 |-  ( ph -> W C_ ( `' F " A ) )
182 11 cvmsrcl 
 |-  ( T e. ( S ` A ) -> A e. J )
183 13 182 syl 
 |-  ( ph -> A e. J )
184 cnima 
 |-  ( ( F e. ( C Cn J ) /\ A e. J ) -> ( `' F " A ) e. C )
185 82 183 184 syl2anc 
 |-  ( ph -> ( `' F " A ) e. C )
186 restopn2 
 |-  ( ( C e. Top /\ ( `' F " A ) e. C ) -> ( W e. ( C |`t ( `' F " A ) ) <-> ( W e. C /\ W C_ ( `' F " A ) ) ) )
187 131 185 186 syl2anc 
 |-  ( ph -> ( W e. ( C |`t ( `' F " A ) ) <-> ( W e. C /\ W C_ ( `' F " A ) ) ) )
188 176 181 187 mpbir2and 
 |-  ( ph -> W e. ( C |`t ( `' F " A ) ) )
189 11 cvmscld 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` A ) /\ W e. T ) -> W e. ( Clsd ` ( C |`t ( `' F " A ) ) ) )
190 3 13 175 189 syl3anc 
 |-  ( ph -> W e. ( Clsd ` ( C |`t ( `' F " A ) ) ) )
191 45 a1i 
 |-  ( ph -> 0 e. ( 0 [,] 1 ) )
192 174 simprd 
 |-  ( ph -> ( H ` X ) e. W )
193 79 192 eqeltrd 
 |-  ( ph -> ( I ` 0 ) e. W )
194 42 129 169 188 190 191 193 conncn 
 |-  ( ph -> I : ( 0 [,] 1 ) --> W )
195 1elunit 
 |-  1 e. ( 0 [,] 1 )
196 ffvelrn 
 |-  ( ( I : ( 0 [,] 1 ) --> W /\ 1 e. ( 0 [,] 1 ) ) -> ( I ` 1 ) e. W )
197 194 195 196 sylancl 
 |-  ( ph -> ( I ` 1 ) e. W )
198 127 197 eqeltrd 
 |-  ( ph -> ( H ` Z ) e. W )