Metamath Proof Explorer

Theorem cvmlift3lem8

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 6-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 ) ) ) ) } )
Assertion cvmlift3lem8 
|- ( ph -> H e. ( K Cn C ) )

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 cvmlift3lem3 
 |-  ( ph -> H : Y --> B )
13 3 adantr 
 |-  ( ( ph /\ y e. Y ) -> F e. ( C CovMap J ) )
14 eqid 
 |-  U. J = U. J
15 2 14 cnf 
 |-  ( G e. ( K Cn J ) -> G : Y --> U. J )
16 7 15 syl 
 |-  ( ph -> G : Y --> U. J )
17 16 ffvelcdmda 
 |-  ( ( ph /\ y e. Y ) -> ( G ` y ) e. U. J )
18 11 14 cvmcov 
 |-  ( ( F e. ( C CovMap J ) /\ ( G ` y ) e. U. J ) -> E. a e. J ( ( G ` y ) e. a /\ ( S ` a ) =/= (/) ) )
19 13 17 18 syl2anc 
 |-  ( ( ph /\ y e. Y ) -> E. a e. J ( ( G ` y ) e. a /\ ( S ` a ) =/= (/) ) )
20 n0 
 |-  ( ( S ` a ) =/= (/) <-> E. t t e. ( S ` a ) )
21 5 ad2antrr 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> K e. N-Locally PConn )
22 7 ad2antrr 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> G e. ( K Cn J ) )
23 simprr 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> t e. ( S ` a ) )
24 11 cvmsrcl 
 |-  ( t e. ( S ` a ) -> a e. J )
25 23 24 syl 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> a e. J )
26 cnima 
 |-  ( ( G e. ( K Cn J ) /\ a e. J ) -> ( `' G " a ) e. K )
27 22 25 26 syl2anc 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> ( `' G " a ) e. K )
28 simplr 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> y e. Y )
29 simprl 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> ( G ` y ) e. a )
30 ffn 
 |-  ( G : Y --> U. J -> G Fn Y )
31 elpreima 
 |-  ( G Fn Y -> ( y e. ( `' G " a ) <-> ( y e. Y /\ ( G ` y ) e. a ) ) )
32 22 15 30 31 4syl 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> ( y e. ( `' G " a ) <-> ( y e. Y /\ ( G ` y ) e. a ) ) )
33 28 29 32 mpbir2and 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> y e. ( `' G " a ) )
34 nlly2i 
 |-  ( ( K e. N-Locally PConn /\ ( `' G " a ) e. K /\ y e. ( `' G " a ) ) -> E. m e. ~P ( `' G " a ) E. v e. K ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) )
35 21 27 33 34 syl3anc 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> E. m e. ~P ( `' G " a ) E. v e. K ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) )
36 3 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> F e. ( C CovMap J ) )
37 4 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> K e. SConn )
38 5 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> K e. N-Locally PConn )
39 6 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> O e. Y )
40 7 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> G e. ( K Cn J ) )
41 8 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> P e. B )
42 9 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> ( F ` P ) = ( G ` O ) )
43 29 adantr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> ( G ` y ) e. a )
44 23 adantr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> t e. ( S ` a ) )
45 simprll 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> m e. ~P ( `' G " a ) )
46 45 elpwid 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> m C_ ( `' G " a ) )
47 eqid 
 |-  ( iota_ b e. t ( H ` y ) e. b ) = ( iota_ b e. t ( H ` y ) e. b )
48 simprr3 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> ( K |`t m ) e. PConn )
49 simprlr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> v e. K )
50 simprr2 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> v C_ m )
51 simprr1 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> y e. v )
52 1 2 36 37 38 39 40 41 42 10 11 43 44 46 47 48 49 50 51 cvmlift3lem7 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( m e. ~P ( `' G " a ) /\ v e. K ) /\ ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) ) ) -> H e. ( ( K CnP C ) ` y ) )
53 52 expr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) /\ ( m e. ~P ( `' G " a ) /\ v e. K ) ) -> ( ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) -> H e. ( ( K CnP C ) ` y ) ) )
54 53 rexlimdvva 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> ( E. m e. ~P ( `' G " a ) E. v e. K ( y e. v /\ v C_ m /\ ( K |`t m ) e. PConn ) -> H e. ( ( K CnP C ) ` y ) ) )
55 35 54 mpd 
 |-  ( ( ( ph /\ y e. Y ) /\ ( ( G ` y ) e. a /\ t e. ( S ` a ) ) ) -> H e. ( ( K CnP C ) ` y ) )
56 55 expr 
 |-  ( ( ( ph /\ y e. Y ) /\ ( G ` y ) e. a ) -> ( t e. ( S ` a ) -> H e. ( ( K CnP C ) ` y ) ) )
57 56 exlimdv 
 |-  ( ( ( ph /\ y e. Y ) /\ ( G ` y ) e. a ) -> ( E. t t e. ( S ` a ) -> H e. ( ( K CnP C ) ` y ) ) )
58 20 57 biimtrid 
 |-  ( ( ( ph /\ y e. Y ) /\ ( G ` y ) e. a ) -> ( ( S ` a ) =/= (/) -> H e. ( ( K CnP C ) ` y ) ) )
59 58 expimpd 
 |-  ( ( ph /\ y e. Y ) -> ( ( ( G ` y ) e. a /\ ( S ` a ) =/= (/) ) -> H e. ( ( K CnP C ) ` y ) ) )
60 59 rexlimdvw 
 |-  ( ( ph /\ y e. Y ) -> ( E. a e. J ( ( G ` y ) e. a /\ ( S ` a ) =/= (/) ) -> H e. ( ( K CnP C ) ` y ) ) )
61 19 60 mpd 
 |-  ( ( ph /\ y e. Y ) -> H e. ( ( K CnP C ) ` y ) )
62 61 ralrimiva 
 |-  ( ph -> A. y e. Y H e. ( ( K CnP C ) ` y ) )
63 sconntop 
 |-  ( K e. SConn -> K e. Top )
64 4 63 syl 
 |-  ( ph -> K e. Top )
65 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
66 64 65 sylib 
 |-  ( ph -> K e. ( TopOn ` Y ) )
67 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
68 3 67 syl 
 |-  ( ph -> C e. Top )
69 1 toptopon 
 |-  ( C e. Top <-> C e. ( TopOn ` B ) )
70 68 69 sylib 
 |-  ( ph -> C e. ( TopOn ` B ) )
71 cncnp 
 |-  ( ( K e. ( TopOn ` Y ) /\ C e. ( TopOn ` B ) ) -> ( H e. ( K Cn C ) <-> ( H : Y --> B /\ A. y e. Y H e. ( ( K CnP C ) ` y ) ) ) )
72 66 70 71 syl2anc 
 |-  ( ph -> ( H e. ( K Cn C ) <-> ( H : Y --> B /\ A. y e. Y H e. ( ( K CnP C ) ` y ) ) ) )
73 12 62 72 mpbir2and 
 |-  ( ph -> H e. ( K Cn C ) )