# Metamath Proof Explorer

## Theorem cvmlift2lem4

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-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)$
cvmlift2.k ${⊢}{K}=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({x}\right)\right)\right)\left({y}\right)\right)$
Assertion cvmlift2lem4 ${⊢}\left({X}\in \left[0,1\right]\wedge {Y}\in \left[0,1\right]\right)\to {X}{K}{Y}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)\left({Y}\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 cvmlift2.k ${⊢}{K}=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({x}\right)\right)\right)\left({y}\right)\right)$
8 oveq1 ${⊢}{x}={X}\to {x}{G}{z}={X}{G}{z}$
9 8 mpteq2dv ${⊢}{x}={X}\to \left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)$
10 9 eqeq2d ${⊢}{x}={X}\to \left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)↔{F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\right)$
11 fveq2 ${⊢}{x}={X}\to {H}\left({x}\right)={H}\left({X}\right)$
12 11 eqeq2d ${⊢}{x}={X}\to \left({f}\left(0\right)={H}\left({x}\right)↔{f}\left(0\right)={H}\left({X}\right)\right)$
13 10 12 anbi12d ${⊢}{x}={X}\to \left(\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({x}\right)\right)↔\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)$
14 13 riotabidv ${⊢}{x}={X}\to \left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({x}\right)\right)\right)=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)$
15 14 fveq1d ${⊢}{x}={X}\to \left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({x}\right)\right)\right)\left({y}\right)=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)\left({y}\right)$
16 fveq2 ${⊢}{y}={Y}\to \left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)\left({y}\right)=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)\left({Y}\right)$
17 fvex ${⊢}\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)\left({Y}\right)\in \mathrm{V}$
18 15 16 7 17 ovmpo ${⊢}\left({X}\in \left[0,1\right]\wedge {Y}\in \left[0,1\right]\right)\to {X}{K}{Y}=\left(\iota {f}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {f}=\left({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge {f}\left(0\right)={H}\left({X}\right)\right)\right)\left({Y}\right)$