# Metamath Proof Explorer

## Theorem cvmlift2lem2

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

Ref Expression
Hypotheses cvmlift2.b ${⊢}{B}=\bigcup {C}$
cvmlift2.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
cvmlift2.g ${⊢}{\phi }\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
cvmlift2.p ${⊢}{\phi }\to {P}\in {B}$
cvmlift2.i ${⊢}{\phi }\to {F}\left({P}\right)=0{G}0$
cvmlift2.h ${⊢}{H}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {f}\left(0\right)={P}\right)\right)$
Assertion cvmlift2lem2 ${⊢}{\phi }\to \left({H}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)\wedge {F}\circ {H}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {H}\left(0\right)={P}\right)$

### Proof

Step Hyp Ref Expression
1 cvmlift2.b ${⊢}{B}=\bigcup {C}$
2 cvmlift2.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
3 cvmlift2.g ${⊢}{\phi }\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
4 cvmlift2.p ${⊢}{\phi }\to {P}\in {B}$
5 cvmlift2.i ${⊢}{\phi }\to {F}\left({P}\right)=0{G}0$
6 cvmlift2.h ${⊢}{H}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {f}\left(0\right)={P}\right)\right)$
7 iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
8 7 a1i ${⊢}{\phi }\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
9 8 cnmptid ${⊢}{\phi }\to \left({z}\in \left[0,1\right]⟼{z}\right)\in \left(\mathrm{II}\mathrm{Cn}\mathrm{II}\right)$
10 0elunit ${⊢}0\in \left[0,1\right]$
11 10 a1i ${⊢}{\phi }\to 0\in \left[0,1\right]$
12 8 8 11 cnmptc ${⊢}{\phi }\to \left({z}\in \left[0,1\right]⟼0\right)\in \left(\mathrm{II}\mathrm{Cn}\mathrm{II}\right)$
13 8 9 12 3 cnmpt12f ${⊢}{\phi }\to \left({z}\in \left[0,1\right]⟼{z}{G}0\right)\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
14 oveq1 ${⊢}{z}=0\to {z}{G}0=0{G}0$
15 eqid ${⊢}\left({z}\in \left[0,1\right]⟼{z}{G}0\right)=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)$
16 ovex ${⊢}0{G}0\in \mathrm{V}$
17 14 15 16 fvmpt ${⊢}0\in \left[0,1\right]\to \left({z}\in \left[0,1\right]⟼{z}{G}0\right)\left(0\right)=0{G}0$
18 10 17 ax-mp ${⊢}\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\left(0\right)=0{G}0$
19 5 18 syl6eqr ${⊢}{\phi }\to {F}\left({P}\right)=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\left(0\right)$
20 1 6 2 13 4 19 cvmliftiota ${⊢}{\phi }\to \left({H}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)\wedge {F}\circ {H}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {H}\left(0\right)={P}\right)$