# Metamath Proof Explorer

## Theorem cvmlift2lem6

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)$
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 cvmlift2lem6 ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {{K}↾}_{\left(\left\{{X}\right\}×\left[0,1\right]\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left(\left\{{X}\right\}×\left[0,1\right]\right)\right)\mathrm{Cn}{C}\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 1 2 3 4 5 6 7 cvmlift2lem5 ${⊢}{\phi }\to {K}:\left[0,1\right]×\left[0,1\right]⟶{B}$
9 8 adantr ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {K}:\left[0,1\right]×\left[0,1\right]⟶{B}$
10 9 ffnd ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {K}Fn\left(\left[0,1\right]×\left[0,1\right]\right)$
11 fnov ${⊢}{K}Fn\left(\left[0,1\right]×\left[0,1\right]\right)↔{K}=\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{u}{K}{v}\right)$
12 10 11 sylib ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {K}=\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{u}{K}{v}\right)$
13 12 reseq1d ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {{K}↾}_{\left(\left\{{X}\right\}×\left[0,1\right]\right)}={\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{u}{K}{v}\right)↾}_{\left(\left\{{X}\right\}×\left[0,1\right]\right)}$
14 simpr ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {X}\in \left[0,1\right]$
15 14 snssd ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left\{{X}\right\}\subseteq \left[0,1\right]$
16 ssid ${⊢}\left[0,1\right]\subseteq \left[0,1\right]$
17 resmpo ${⊢}\left(\left\{{X}\right\}\subseteq \left[0,1\right]\wedge \left[0,1\right]\subseteq \left[0,1\right]\right)\to {\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{u}{K}{v}\right)↾}_{\left(\left\{{X}\right\}×\left[0,1\right]\right)}=\left({u}\in \left\{{X}\right\},{v}\in \left[0,1\right]⟼{u}{K}{v}\right)$
18 15 16 17 sylancl ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{u}{K}{v}\right)↾}_{\left(\left\{{X}\right\}×\left[0,1\right]\right)}=\left({u}\in \left\{{X}\right\},{v}\in \left[0,1\right]⟼{u}{K}{v}\right)$
19 elsni ${⊢}{u}\in \left\{{X}\right\}\to {u}={X}$
20 19 3ad2ant2 ${⊢}\left(\left({\phi }\wedge {X}\in \left[0,1\right]\right)\wedge {u}\in \left\{{X}\right\}\wedge {v}\in \left[0,1\right]\right)\to {u}={X}$
21 20 oveq1d ${⊢}\left(\left({\phi }\wedge {X}\in \left[0,1\right]\right)\wedge {u}\in \left\{{X}\right\}\wedge {v}\in \left[0,1\right]\right)\to {u}{K}{v}={X}{K}{v}$
22 simp1r ${⊢}\left(\left({\phi }\wedge {X}\in \left[0,1\right]\right)\wedge {u}\in \left\{{X}\right\}\wedge {v}\in \left[0,1\right]\right)\to {X}\in \left[0,1\right]$
23 simp3 ${⊢}\left(\left({\phi }\wedge {X}\in \left[0,1\right]\right)\wedge {u}\in \left\{{X}\right\}\wedge {v}\in \left[0,1\right]\right)\to {v}\in \left[0,1\right]$
24 1 2 3 4 5 6 7 cvmlift2lem4 ${⊢}\left({X}\in \left[0,1\right]\wedge {v}\in \left[0,1\right]\right)\to {X}{K}{v}=\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({v}\right)$
25 22 23 24 syl2anc ${⊢}\left(\left({\phi }\wedge {X}\in \left[0,1\right]\right)\wedge {u}\in \left\{{X}\right\}\wedge {v}\in \left[0,1\right]\right)\to {X}{K}{v}=\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({v}\right)$
26 21 25 eqtrd ${⊢}\left(\left({\phi }\wedge {X}\in \left[0,1\right]\right)\wedge {u}\in \left\{{X}\right\}\wedge {v}\in \left[0,1\right]\right)\to {u}{K}{v}=\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({v}\right)$
27 26 mpoeq3dva ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({u}\in \left\{{X}\right\},{v}\in \left[0,1\right]⟼{u}{K}{v}\right)=\left({u}\in \left\{{X}\right\},{v}\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({v}\right)\right)$
28 18 27 eqtrd ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{u}{K}{v}\right)↾}_{\left(\left\{{X}\right\}×\left[0,1\right]\right)}=\left({u}\in \left\{{X}\right\},{v}\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({v}\right)\right)$
29 13 28 eqtrd ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {{K}↾}_{\left(\left\{{X}\right\}×\left[0,1\right]\right)}=\left({u}\in \left\{{X}\right\},{v}\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({v}\right)\right)$
30 eqid ${⊢}\mathrm{II}{↾}_{𝑡}\left\{{X}\right\}=\mathrm{II}{↾}_{𝑡}\left\{{X}\right\}$
31 iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
32 31 a1i ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
33 eqid ${⊢}\mathrm{II}{↾}_{𝑡}\left[0,1\right]=\mathrm{II}{↾}_{𝑡}\left[0,1\right]$
34 16 a1i ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left[0,1\right]\subseteq \left[0,1\right]$
35 32 32 cnmpt2nd ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼{v}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{II}\right)$
36 eqid ${⊢}\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)$
37 1 2 3 4 5 6 36 cvmlift2lem3 ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left(\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)\in \left(\mathrm{II}\mathrm{Cn}{C}\right)\wedge {F}\circ \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({z}\in \left[0,1\right]⟼{X}{G}{z}\right)\wedge \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(0\right)={H}\left({X}\right)\right)$
38 37 simp1d ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\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)\in \left(\mathrm{II}\mathrm{Cn}{C}\right)$
39 32 32 35 38 cnmpt21f ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({u}\in \left[0,1\right],{v}\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({v}\right)\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{C}\right)$
40 30 32 15 33 32 34 39 cnmpt2res ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({u}\in \left\{{X}\right\},{v}\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({v}\right)\right)\in \left(\left(\left(\mathrm{II}{↾}_{𝑡}\left\{{X}\right\}\right){×}_{t}\left(\mathrm{II}{↾}_{𝑡}\left[0,1\right]\right)\right)\mathrm{Cn}{C}\right)$
41 iitop ${⊢}\mathrm{II}\in \mathrm{Top}$
42 snex ${⊢}\left\{{X}\right\}\in \mathrm{V}$
43 ovex ${⊢}\left[0,1\right]\in \mathrm{V}$
44 txrest ${⊢}\left(\left(\mathrm{II}\in \mathrm{Top}\wedge \mathrm{II}\in \mathrm{Top}\right)\wedge \left(\left\{{X}\right\}\in \mathrm{V}\wedge \left[0,1\right]\in \mathrm{V}\right)\right)\to \left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left(\left\{{X}\right\}×\left[0,1\right]\right)=\left(\mathrm{II}{↾}_{𝑡}\left\{{X}\right\}\right){×}_{t}\left(\mathrm{II}{↾}_{𝑡}\left[0,1\right]\right)$
45 41 41 42 43 44 mp4an ${⊢}\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left(\left\{{X}\right\}×\left[0,1\right]\right)=\left(\mathrm{II}{↾}_{𝑡}\left\{{X}\right\}\right){×}_{t}\left(\mathrm{II}{↾}_{𝑡}\left[0,1\right]\right)$
46 45 oveq1i ${⊢}\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left(\left\{{X}\right\}×\left[0,1\right]\right)\right)\mathrm{Cn}{C}=\left(\left(\mathrm{II}{↾}_{𝑡}\left\{{X}\right\}\right){×}_{t}\left(\mathrm{II}{↾}_{𝑡}\left[0,1\right]\right)\right)\mathrm{Cn}{C}$
47 40 46 syl6eleqr ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to \left({u}\in \left\{{X}\right\},{v}\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({v}\right)\right)\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left(\left\{{X}\right\}×\left[0,1\right]\right)\right)\mathrm{Cn}{C}\right)$
48 29 47 eqeltrd ${⊢}\left({\phi }\wedge {X}\in \left[0,1\right]\right)\to {{K}↾}_{\left(\left\{{X}\right\}×\left[0,1\right]\right)}\in \left(\left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right){↾}_{𝑡}\left(\left\{{X}\right\}×\left[0,1\right]\right)\right)\mathrm{Cn}{C}\right)$