Metamath Proof Explorer

Theorem cvmlift3lem9

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-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 ) ) ) ) } )
Assertion cvmlift3lem9 
|- ( ph -> E. f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) )

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 1 2 3 4 5 6 7 8 9 10 11 cvmlift3lem8 
 |-  ( ph -> H e. ( K Cn C ) )
13 1 2 3 4 5 6 7 8 9 10 cvmlift3lem5 
 |-  ( ph -> ( F o. H ) = G )
14 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
15 14 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
16 sconntop 
 |-  ( K e. SConn -> K e. Top )
17 4 16 syl 
 |-  ( ph -> K e. Top )
18 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
19 17 18 sylib 
 |-  ( ph -> K e. ( TopOn ` Y ) )
20 cnconst2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ K e. ( TopOn ` Y ) /\ O e. Y ) -> ( ( 0 [,] 1 ) X. { O } ) e. ( II Cn K ) )
21 15 19 6 20 syl3anc 
 |-  ( ph -> ( ( 0 [,] 1 ) X. { O } ) e. ( II Cn K ) )
22 0elunit 
 |-  0 e. ( 0 [,] 1 )
23 fvconst2g 
 |-  ( ( O e. Y /\ 0 e. ( 0 [,] 1 ) ) -> ( ( ( 0 [,] 1 ) X. { O } ) ` 0 ) = O )
24 6 22 23 sylancl 
 |-  ( ph -> ( ( ( 0 [,] 1 ) X. { O } ) ` 0 ) = O )
25 1elunit 
 |-  1 e. ( 0 [,] 1 )
26 fvconst2g 
 |-  ( ( O e. Y /\ 1 e. ( 0 [,] 1 ) ) -> ( ( ( 0 [,] 1 ) X. { O } ) ` 1 ) = O )
27 6 25 26 sylancl 
 |-  ( ph -> ( ( ( 0 [,] 1 ) X. { O } ) ` 1 ) = O )
28 9 sneqd 
 |-  ( ph -> { ( F ` P ) } = { ( G ` O ) } )
29 28 xpeq2d 
 |-  ( ph -> ( ( 0 [,] 1 ) X. { ( F ` P ) } ) = ( ( 0 [,] 1 ) X. { ( G ` O ) } ) )
30 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
31 eqid 
 |-  U. J = U. J
32 1 31 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> U. J )
33 ffn 
 |-  ( F : B --> U. J -> F Fn B )
34 3 30 32 33 4syl 
 |-  ( ph -> F Fn B )
35 fcoconst 
 |-  ( ( F Fn B /\ P e. B ) -> ( F o. ( ( 0 [,] 1 ) X. { P } ) ) = ( ( 0 [,] 1 ) X. { ( F ` P ) } ) )
36 34 8 35 syl2anc 
 |-  ( ph -> ( F o. ( ( 0 [,] 1 ) X. { P } ) ) = ( ( 0 [,] 1 ) X. { ( F ` P ) } ) )
37 2 31 cnf 
 |-  ( G e. ( K Cn J ) -> G : Y --> U. J )
38 7 37 syl 
 |-  ( ph -> G : Y --> U. J )
39 38 ffnd 
 |-  ( ph -> G Fn Y )
40 fcoconst 
 |-  ( ( G Fn Y /\ O e. Y ) -> ( G o. ( ( 0 [,] 1 ) X. { O } ) ) = ( ( 0 [,] 1 ) X. { ( G ` O ) } ) )
41 39 6 40 syl2anc 
 |-  ( ph -> ( G o. ( ( 0 [,] 1 ) X. { O } ) ) = ( ( 0 [,] 1 ) X. { ( G ` O ) } ) )
42 29 36 41 3eqtr4d 
 |-  ( ph -> ( F o. ( ( 0 [,] 1 ) X. { P } ) ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) )
43 fvconst2g 
 |-  ( ( P e. B /\ 0 e. ( 0 [,] 1 ) ) -> ( ( ( 0 [,] 1 ) X. { P } ) ` 0 ) = P )
44 8 22 43 sylancl 
 |-  ( ph -> ( ( ( 0 [,] 1 ) X. { P } ) ` 0 ) = P )
45 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
46 3 45 syl 
 |-  ( ph -> C e. Top )
47 1 toptopon 
 |-  ( C e. Top <-> C e. ( TopOn ` B ) )
48 46 47 sylib 
 |-  ( ph -> C e. ( TopOn ` B ) )
49 cnconst2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ C e. ( TopOn ` B ) /\ P e. B ) -> ( ( 0 [,] 1 ) X. { P } ) e. ( II Cn C ) )
50 15 48 8 49 syl3anc 
 |-  ( ph -> ( ( 0 [,] 1 ) X. { P } ) e. ( II Cn C ) )
51 cvmtop2 
 |-  ( F e. ( C CovMap J ) -> J e. Top )
52 3 51 syl 
 |-  ( ph -> J e. Top )
53 31 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
54 52 53 sylib 
 |-  ( ph -> J e. ( TopOn ` U. J ) )
55 38 6 ffvelrnd 
 |-  ( ph -> ( G ` O ) e. U. J )
56 cnconst2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` U. J ) /\ ( G ` O ) e. U. J ) -> ( ( 0 [,] 1 ) X. { ( G ` O ) } ) e. ( II Cn J ) )
57 15 54 55 56 syl3anc 
 |-  ( ph -> ( ( 0 [,] 1 ) X. { ( G ` O ) } ) e. ( II Cn J ) )
58 41 57 eqeltrd 
 |-  ( ph -> ( G o. ( ( 0 [,] 1 ) X. { O } ) ) e. ( II Cn J ) )
59 fvconst2g 
 |-  ( ( ( G ` O ) e. U. J /\ 0 e. ( 0 [,] 1 ) ) -> ( ( ( 0 [,] 1 ) X. { ( G ` O ) } ) ` 0 ) = ( G ` O ) )
60 55 22 59 sylancl 
 |-  ( ph -> ( ( ( 0 [,] 1 ) X. { ( G ` O ) } ) ` 0 ) = ( G ` O ) )
61 41 fveq1d 
 |-  ( ph -> ( ( G o. ( ( 0 [,] 1 ) X. { O } ) ) ` 0 ) = ( ( ( 0 [,] 1 ) X. { ( G ` O ) } ) ` 0 ) )
62 60 61 9 3eqtr4rd 
 |-  ( ph -> ( F ` P ) = ( ( G o. ( ( 0 [,] 1 ) X. { O } ) ) ` 0 ) )
63 1 cvmlift 
 |-  ( ( ( F e. ( C CovMap J ) /\ ( G o. ( ( 0 [,] 1 ) X. { O } ) ) e. ( II Cn J ) ) /\ ( P e. B /\ ( F ` P ) = ( ( G o. ( ( 0 [,] 1 ) X. { O } ) ) ` 0 ) ) ) -> E! g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) )
64 3 58 8 62 63 syl22anc 
 |-  ( ph -> E! g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) )
65 coeq2 
 |-  ( g = ( ( 0 [,] 1 ) X. { P } ) -> ( F o. g ) = ( F o. ( ( 0 [,] 1 ) X. { P } ) ) )
66 65 eqeq1d 
 |-  ( g = ( ( 0 [,] 1 ) X. { P } ) -> ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) <-> ( F o. ( ( 0 [,] 1 ) X. { P } ) ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) ) )
67 fveq1 
 |-  ( g = ( ( 0 [,] 1 ) X. { P } ) -> ( g ` 0 ) = ( ( ( 0 [,] 1 ) X. { P } ) ` 0 ) )
68 67 eqeq1d 
 |-  ( g = ( ( 0 [,] 1 ) X. { P } ) -> ( ( g ` 0 ) = P <-> ( ( ( 0 [,] 1 ) X. { P } ) ` 0 ) = P ) )
69 66 68 anbi12d 
 |-  ( g = ( ( 0 [,] 1 ) X. { P } ) -> ( ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) <-> ( ( F o. ( ( 0 [,] 1 ) X. { P } ) ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( ( ( 0 [,] 1 ) X. { P } ) ` 0 ) = P ) ) )
70 69 riota2 
 |-  ( ( ( ( 0 [,] 1 ) X. { P } ) e. ( II Cn C ) /\ E! g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) -> ( ( ( F o. ( ( 0 [,] 1 ) X. { P } ) ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( ( ( 0 [,] 1 ) X. { P } ) ` 0 ) = P ) <-> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) = ( ( 0 [,] 1 ) X. { P } ) ) )
71 50 64 70 syl2anc 
 |-  ( ph -> ( ( ( F o. ( ( 0 [,] 1 ) X. { P } ) ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( ( ( 0 [,] 1 ) X. { P } ) ` 0 ) = P ) <-> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) = ( ( 0 [,] 1 ) X. { P } ) ) )
72 42 44 71 mpbi2and 
 |-  ( ph -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) = ( ( 0 [,] 1 ) X. { P } ) )
73 72 fveq1d 
 |-  ( ph -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( ( 0 [,] 1 ) X. { P } ) ` 1 ) )
74 fvconst2g 
 |-  ( ( P e. B /\ 1 e. ( 0 [,] 1 ) ) -> ( ( ( 0 [,] 1 ) X. { P } ) ` 1 ) = P )
75 8 25 74 sylancl 
 |-  ( ph -> ( ( ( 0 [,] 1 ) X. { P } ) ` 1 ) = P )
76 73 75 eqtrd 
 |-  ( ph -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P )
77 fveq1 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( f ` 0 ) = ( ( ( 0 [,] 1 ) X. { O } ) ` 0 ) )
78 77 eqeq1d 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( ( f ` 0 ) = O <-> ( ( ( 0 [,] 1 ) X. { O } ) ` 0 ) = O ) )
79 fveq1 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( f ` 1 ) = ( ( ( 0 [,] 1 ) X. { O } ) ` 1 ) )
80 79 eqeq1d 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( ( f ` 1 ) = O <-> ( ( ( 0 [,] 1 ) X. { O } ) ` 1 ) = O ) )
81 coeq2 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( G o. f ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) )
82 81 eqeq2d 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( ( F o. g ) = ( G o. f ) <-> ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) ) )
83 82 anbi1d 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) <-> ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) )
84 83 riotabidv 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( 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. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) )
85 84 fveq1d 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( ( 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. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) )
86 85 eqeq1d 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P <-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P ) )
87 78 80 86 3anbi123d 
 |-  ( f = ( ( 0 [,] 1 ) X. { O } ) -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = O /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P ) <-> ( ( ( ( 0 [,] 1 ) X. { O } ) ` 0 ) = O /\ ( ( ( 0 [,] 1 ) X. { O } ) ` 1 ) = O /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P ) ) )
88 87 rspcev 
 |-  ( ( ( ( 0 [,] 1 ) X. { O } ) e. ( II Cn K ) /\ ( ( ( ( 0 [,] 1 ) X. { O } ) ` 0 ) = O /\ ( ( ( 0 [,] 1 ) X. { O } ) ` 1 ) = O /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. ( ( 0 [,] 1 ) X. { O } ) ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = O /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P ) )
89 21 24 27 76 88 syl13anc 
 |-  ( ph -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = O /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P ) )
90 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 
 |-  ( ( ph /\ O e. Y ) -> ( ( H ` O ) = P <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = O /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P ) ) )
91 6 90 mpdan 
 |-  ( ph -> ( ( H ` O ) = P <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = O /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = P ) ) )
92 89 91 mpbird 
 |-  ( ph -> ( H ` O ) = P )
93 coeq2 
 |-  ( f = H -> ( F o. f ) = ( F o. H ) )
94 93 eqeq1d 
 |-  ( f = H -> ( ( F o. f ) = G <-> ( F o. H ) = G ) )
95 fveq1 
 |-  ( f = H -> ( f ` O ) = ( H ` O ) )
96 95 eqeq1d 
 |-  ( f = H -> ( ( f ` O ) = P <-> ( H ` O ) = P ) )
97 94 96 anbi12d 
 |-  ( f = H -> ( ( ( F o. f ) = G /\ ( f ` O ) = P ) <-> ( ( F o. H ) = G /\ ( H ` O ) = P ) ) )
98 97 rspcev 
 |-  ( ( H e. ( K Cn C ) /\ ( ( F o. H ) = G /\ ( H ` O ) = P ) ) -> E. f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) )
99 12 13 92 98 syl12anc 
 |-  ( ph -> E. f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) )