Metamath Proof Explorer

Theorem cvmlift3lem4

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 ) ) )
Assertion cvmlift3lem4 
|- ( ( ph /\ X e. Y ) -> ( ( H ` X ) = A <-> 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 ) = A ) ) )

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 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 
 |-  ( ph -> H : Y --> B )
12 11 ffvelcdmda 
 |-  ( ( ph /\ X e. Y ) -> ( H ` X ) e. B )
13 eleq1 
 |-  ( ( H ` X ) = A -> ( ( H ` X ) e. B <-> A e. B ) )
14 12 13 syl5ibcom 
 |-  ( ( ph /\ X e. Y ) -> ( ( H ` X ) = A -> A e. B ) )
15 eqid 
 |-  ( 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. f ) /\ ( g ` 0 ) = P ) )
16 3 ad2antrr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> F e. ( C CovMap J ) )
17 simprl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> f e. ( II Cn K ) )
18 7 ad2antrr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> G e. ( K Cn J ) )
19 cnco 
 |-  ( ( f e. ( II Cn K ) /\ G e. ( K Cn J ) ) -> ( G o. f ) e. ( II Cn J ) )
20 17 18 19 syl2anc 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( G o. f ) e. ( II Cn J ) )
21 8 ad2antrr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> P e. B )
22 simprr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( f ` 0 ) = O )
23 22 fveq2d 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( G ` ( f ` 0 ) ) = ( G ` O ) )
24 iiuni 
 |-  ( 0 [,] 1 ) = U. II
25 24 2 cnf 
 |-  ( f e. ( II Cn K ) -> f : ( 0 [,] 1 ) --> Y )
26 17 25 syl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> f : ( 0 [,] 1 ) --> Y )
27 0elunit 
 |-  0 e. ( 0 [,] 1 )
28 fvco3 
 |-  ( ( f : ( 0 [,] 1 ) --> Y /\ 0 e. ( 0 [,] 1 ) ) -> ( ( G o. f ) ` 0 ) = ( G ` ( f ` 0 ) ) )
29 26 27 28 sylancl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( ( G o. f ) ` 0 ) = ( G ` ( f ` 0 ) ) )
30 9 ad2antrr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( F ` P ) = ( G ` O ) )
31 23 29 30 3eqtr4rd 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( F ` P ) = ( ( G o. f ) ` 0 ) )
32 1 15 16 20 21 31 cvmliftiota 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) e. ( II Cn C ) /\ ( F o. ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ) = ( G o. f ) /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 0 ) = P ) )
33 32 simp1d 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) e. ( II Cn C ) )
34 24 1 cnf 
 |-  ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) e. ( II Cn C ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) : ( 0 [,] 1 ) --> B )
35 33 34 syl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) : ( 0 [,] 1 ) --> B )
36 1elunit 
 |-  1 e. ( 0 [,] 1 )
37 ffvelcdm 
 |-  ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) : ( 0 [,] 1 ) --> B /\ 1 e. ( 0 [,] 1 ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) e. B )
38 35 36 37 sylancl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) e. B )
39 eleq1 
 |-  ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = A -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) e. B <-> A e. B ) )
40 38 39 syl5ibcom 
 |-  ( ( ( ph /\ X e. Y ) /\ ( f e. ( II Cn K ) /\ ( f ` 0 ) = O ) ) -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = A -> A e. B ) )
41 40 expr 
 |-  ( ( ( ph /\ X e. Y ) /\ f e. ( II Cn K ) ) -> ( ( f ` 0 ) = O -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = A -> A e. B ) ) )
42 41 a1dd 
 |-  ( ( ( ph /\ X e. Y ) /\ 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 ) = A -> A e. B ) ) ) )
43 42 3impd 
 |-  ( ( ( ph /\ X e. Y ) /\ 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 ) = A ) -> A e. B ) )
44 43 rexlimdva 
 |-  ( ( 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 ) = A ) -> A e. B ) )
45 eqeq2 
 |-  ( x = X -> ( ( f ` 1 ) = x <-> ( f ` 1 ) = X ) )
46 45 3anbi2d 
 |-  ( x = X -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
47 46 rexbidv 
 |-  ( x = 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 ) = z ) <-> 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 ) ) )
48 47 riotabidv 
 |-  ( x = X -> ( 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 ) ) = ( 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 ) ) )
49 riotaex 
 |-  ( 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 ) ) e. _V
50 48 10 49 fvmpt 
 |-  ( X e. Y -> ( H ` X ) = ( 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 ) ) )
51 50 adantl 
 |-  ( ( ph /\ X e. Y ) -> ( H ` X ) = ( 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 ) ) )
52 51 eqeq1d 
 |-  ( ( ph /\ X e. Y ) -> ( ( H ` X ) = A <-> ( 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 ) ) = A ) )
53 52 adantl 
 |-  ( ( A e. B /\ ( ph /\ X e. Y ) ) -> ( ( H ` X ) = A <-> ( 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 ) ) = A ) )
54 1 2 3 4 5 6 7 8 9 cvmlift3lem2 
 |-  ( ( ph /\ X e. Y ) -> E! 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 ) )
55 eqeq2 
 |-  ( z = A -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z <-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = A ) )
56 55 3anbi3d 
 |-  ( z = A -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = A ) ) )
57 56 rexbidv 
 |-  ( z = A -> ( 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 ) <-> 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 ) = A ) ) )
58 57 riota2 
 |-  ( ( A e. B /\ E! 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 ) ) -> ( 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 ) = A ) <-> ( 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 ) ) = A ) )
59 54 58 sylan2 
 |-  ( ( A e. B /\ ( 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 ) = A ) <-> ( 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 ) ) = A ) )
60 53 59 bitr4d 
 |-  ( ( A e. B /\ ( ph /\ X e. Y ) ) -> ( ( H ` X ) = A <-> 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 ) = A ) ) )
61 60 expcom 
 |-  ( ( ph /\ X e. Y ) -> ( A e. B -> ( ( H ` X ) = A <-> 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 ) = A ) ) ) )
62 14 44 61 pm5.21ndd 
 |-  ( ( ph /\ X e. Y ) -> ( ( H ` X ) = A <-> 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 ) = A ) ) )