Metamath Proof Explorer

Theorem cvmlift2lem7

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmlift2.b 
|- B = U. C
cvmlift2.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmlift2.g 
|- ( ph -> G e. ( ( II tX II ) Cn J ) )
cvmlift2.p 
|- ( ph -> P e. B )
cvmlift2.i 
|- ( ph -> ( F ` P ) = ( 0 G 0 ) )
cvmlift2.h 
|- H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( f ` 0 ) = P ) )
cvmlift2.k 
|- K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) )
Assertion cvmlift2lem7 
|- ( ph -> ( F o. K ) = G )

Proof

Step Hyp Ref Expression
1 cvmlift2.b 
 |-  B = U. C
2 cvmlift2.f 
 |-  ( ph -> F e. ( C CovMap J ) )
3 cvmlift2.g 
 |-  ( ph -> G e. ( ( II tX II ) Cn J ) )
4 cvmlift2.p 
 |-  ( ph -> P e. B )
5 cvmlift2.i 
 |-  ( ph -> ( F ` P ) = ( 0 G 0 ) )
6 cvmlift2.h 
 |-  H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( f ` 0 ) = P ) )
7 cvmlift2.k 
 |-  K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) )
8 eqid 
 |-  ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) )
9 1 2 3 4 5 6 8 cvmlift2lem3 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) e. ( II Cn C ) /\ ( F o. ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` 0 ) = ( H ` x ) ) )
10 9 adantrr 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) e. ( II Cn C ) /\ ( F o. ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` 0 ) = ( H ` x ) ) )
11 10 simp2d 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( F o. ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) )
12 11 fveq1d 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( F o. ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ) ` y ) = ( ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) ` y ) )
13 10 simp1d 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) e. ( II Cn C ) )
14 iiuni 
 |-  ( 0 [,] 1 ) = U. II
15 14 1 cnf 
 |-  ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) e. ( II Cn C ) -> ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) : ( 0 [,] 1 ) --> B )
16 13 15 syl 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) : ( 0 [,] 1 ) --> B )
17 simprr 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> y e. ( 0 [,] 1 ) )
18 fvco3 
 |-  ( ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) : ( 0 [,] 1 ) --> B /\ y e. ( 0 [,] 1 ) ) -> ( ( F o. ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ) ` y ) = ( F ` ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) ) )
19 16 17 18 syl2anc 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( F o. ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ) ` y ) = ( F ` ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) ) )
20 oveq2 
 |-  ( z = y -> ( x G z ) = ( x G y ) )
21 eqid 
 |-  ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) )
22 ovex 
 |-  ( x G y ) e. _V
23 20 21 22 fvmpt 
 |-  ( y e. ( 0 [,] 1 ) -> ( ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) ` y ) = ( x G y ) )
24 17 23 syl 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) ` y ) = ( x G y ) )
25 12 19 24 3eqtr3d 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) ) = ( x G y ) )
26 25 3impb 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) -> ( F ` ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) ) = ( x G y ) )
27 26 mpoeq3dva 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) ) ) = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x G y ) ) )
28 16 17 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) ) -> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) e. B )
29 7 a1i 
 |-  ( ph -> K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) ) )
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 2 30 32 3syl 
 |-  ( ph -> F : B --> U. J )
34 33 feqmptd 
 |-  ( ph -> F = ( w e. B |-> ( F ` w ) ) )
35 fveq2 
 |-  ( w = ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) -> ( F ` w ) = ( F ` ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) ) )
36 28 29 34 35 fmpoco 
 |-  ( ph -> ( F o. K ) = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) ) ) )
37 iitop 
 |-  II e. Top
38 37 37 14 14 txunii 
 |-  ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) = U. ( II tX II )
39 38 31 cnf 
 |-  ( G e. ( ( II tX II ) Cn J ) -> G : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> U. J )
40 ffn 
 |-  ( G : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> U. J -> G Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
41 3 39 40 3syl 
 |-  ( ph -> G Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
42 fnov 
 |-  ( G Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) <-> G = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x G y ) ) )
43 41 42 sylib 
 |-  ( ph -> G = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x G y ) ) )
44 27 36 43 3eqtr4d 
 |-  ( ph -> ( F o. K ) = G )