Metamath Proof Explorer

Theorem cvmlift2lem3

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 ) )
cvmlift2lem3.1 
|- K = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) )
Assertion cvmlift2lem3 
|- ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( K e. ( II Cn C ) /\ ( F o. K ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( K ` 0 ) = ( H ` X ) ) )

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 cvmlift2lem3.1 
 |-  K = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) )
8 2 adantr 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> F e. ( C CovMap J ) )
9 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
10 9 a1i 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
11 simpr 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> X e. ( 0 [,] 1 ) )
12 10 10 11 cnmptc 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( z e. ( 0 [,] 1 ) |-> X ) e. ( II Cn II ) )
13 10 cnmptid 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( z e. ( 0 [,] 1 ) |-> z ) e. ( II Cn II ) )
14 3 adantr 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> G e. ( ( II tX II ) Cn J ) )
15 10 12 13 14 cnmpt12f 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) e. ( II Cn J ) )
16 1 2 3 4 5 6 cvmlift2lem2 
 |-  ( ph -> ( H e. ( II Cn C ) /\ ( F o. H ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( H ` 0 ) = P ) )
17 16 simp1d 
 |-  ( ph -> H e. ( II Cn C ) )
18 iiuni 
 |-  ( 0 [,] 1 ) = U. II
19 18 1 cnf 
 |-  ( H e. ( II Cn C ) -> H : ( 0 [,] 1 ) --> B )
20 17 19 syl 
 |-  ( ph -> H : ( 0 [,] 1 ) --> B )
21 20 ffvelcdmda 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( H ` X ) e. B )
22 0elunit 
 |-  0 e. ( 0 [,] 1 )
23 oveq2 
 |-  ( z = 0 -> ( X G z ) = ( X G 0 ) )
24 eqid 
 |-  ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) )
25 ovex 
 |-  ( X G 0 ) e. _V
26 23 24 25 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) ` 0 ) = ( X G 0 ) )
27 22 26 mp1i 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) ` 0 ) = ( X G 0 ) )
28 16 simp2d 
 |-  ( ph -> ( F o. H ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) )
29 28 fveq1d 
 |-  ( ph -> ( ( F o. H ) ` X ) = ( ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) ` X ) )
30 oveq1 
 |-  ( z = X -> ( z G 0 ) = ( X G 0 ) )
31 eqid 
 |-  ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) )
32 30 31 25 fvmpt 
 |-  ( X e. ( 0 [,] 1 ) -> ( ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) ` X ) = ( X G 0 ) )
33 29 32 sylan9eq 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( F o. H ) ` X ) = ( X G 0 ) )
34 fvco3 
 |-  ( ( H : ( 0 [,] 1 ) --> B /\ X e. ( 0 [,] 1 ) ) -> ( ( F o. H ) ` X ) = ( F ` ( H ` X ) ) )
35 20 34 sylan 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( F o. H ) ` X ) = ( F ` ( H ` X ) ) )
36 27 33 35 3eqtr2rd 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( F ` ( H ` X ) ) = ( ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) ` 0 ) )
37 1 7 8 15 21 36 cvmliftiota 
 |-  ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( K e. ( II Cn C ) /\ ( F o. K ) = ( z e. ( 0 [,] 1 ) |-> ( X G z ) ) /\ ( K ` 0 ) = ( H ` X ) ) )