# 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 ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ffvelrnda
` |-  ( ( 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 ) ) )`