# Metamath Proof Explorer

## Theorem cvmlift3lem7

Description: Lemma for cvmlift3 . (Contributed by Mario Carneiro, 9-Jul-2015)

Ref Expression
Hypotheses cvmlift3.b ${⊢}{B}=\bigcup {C}$
cvmlift3.y ${⊢}{Y}=\bigcup {K}$
cvmlift3.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
cvmlift3.k ${⊢}{\phi }\to {K}\in \mathrm{SConn}$
cvmlift3.l ${⊢}{\phi }\to {K}\in N-Locally\mathrm{PConn}$
cvmlift3.o ${⊢}{\phi }\to {O}\in {Y}$
cvmlift3.g ${⊢}{\phi }\to {G}\in \left({K}\mathrm{Cn}{J}\right)$
cvmlift3.p ${⊢}{\phi }\to {P}\in {B}$
cvmlift3.e ${⊢}{\phi }\to {F}\left({P}\right)={G}\left({O}\right)$
cvmlift3.h ${⊢}{H}=\left({x}\in {Y}⟼\left(\iota {z}\in {B}|\exists {f}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={O}\wedge {f}\left(1\right)={x}\wedge \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)={z}\right)\right)\right)$
cvmlift3lem7.s ${⊢}{S}=\left({k}\in {J}⟼\left\{{s}\in \left(𝒫{C}\setminus \left\{\varnothing \right\}\right)|\left(\bigcup {s}={{F}}^{-1}\left[{k}\right]\wedge \forall {c}\in {s}\phantom{\rule{.4em}{0ex}}\left(\forall {d}\in \left({s}\setminus \left\{{c}\right\}\right)\phantom{\rule{.4em}{0ex}}{c}\cap {d}=\varnothing \wedge {{F}↾}_{{c}}\in \left(\left({C}{↾}_{𝑡}{c}\right)\mathrm{Homeo}\left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)\right\}\right)$
cvmlift3lem7.1 ${⊢}{\phi }\to {G}\left({X}\right)\in {A}$
cvmlift3lem7.2 ${⊢}{\phi }\to {T}\in {S}\left({A}\right)$
cvmlift3lem7.3 ${⊢}{\phi }\to {M}\subseteq {{G}}^{-1}\left[{A}\right]$
cvmlift3lem7.w ${⊢}{W}=\left(\iota {b}\in {T}|{H}\left({X}\right)\in {b}\right)$
cvmlift3lem7.7 ${⊢}{\phi }\to {K}{↾}_{𝑡}{M}\in \mathrm{PConn}$
cvmlift3lem7.4 ${⊢}{\phi }\to {V}\in {K}$
cvmlift3lem7.5 ${⊢}{\phi }\to {V}\subseteq {M}$
cvmlift3lem7.6 ${⊢}{\phi }\to {X}\in {V}$
Assertion cvmlift3lem7 ${⊢}{\phi }\to {H}\in \left({K}\mathrm{CnP}{C}\right)\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 cvmlift3.b ${⊢}{B}=\bigcup {C}$
2 cvmlift3.y ${⊢}{Y}=\bigcup {K}$
3 cvmlift3.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
4 cvmlift3.k ${⊢}{\phi }\to {K}\in \mathrm{SConn}$
5 cvmlift3.l ${⊢}{\phi }\to {K}\in N-Locally\mathrm{PConn}$
6 cvmlift3.o ${⊢}{\phi }\to {O}\in {Y}$
7 cvmlift3.g ${⊢}{\phi }\to {G}\in \left({K}\mathrm{Cn}{J}\right)$
8 cvmlift3.p ${⊢}{\phi }\to {P}\in {B}$
9 cvmlift3.e ${⊢}{\phi }\to {F}\left({P}\right)={G}\left({O}\right)$
10 cvmlift3.h ${⊢}{H}=\left({x}\in {Y}⟼\left(\iota {z}\in {B}|\exists {f}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={O}\wedge {f}\left(1\right)={x}\wedge \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)={z}\right)\right)\right)$
11 cvmlift3lem7.s ${⊢}{S}=\left({k}\in {J}⟼\left\{{s}\in \left(𝒫{C}\setminus \left\{\varnothing \right\}\right)|\left(\bigcup {s}={{F}}^{-1}\left[{k}\right]\wedge \forall {c}\in {s}\phantom{\rule{.4em}{0ex}}\left(\forall {d}\in \left({s}\setminus \left\{{c}\right\}\right)\phantom{\rule{.4em}{0ex}}{c}\cap {d}=\varnothing \wedge {{F}↾}_{{c}}\in \left(\left({C}{↾}_{𝑡}{c}\right)\mathrm{Homeo}\left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)\right\}\right)$
12 cvmlift3lem7.1 ${⊢}{\phi }\to {G}\left({X}\right)\in {A}$
13 cvmlift3lem7.2 ${⊢}{\phi }\to {T}\in {S}\left({A}\right)$
14 cvmlift3lem7.3 ${⊢}{\phi }\to {M}\subseteq {{G}}^{-1}\left[{A}\right]$
15 cvmlift3lem7.w ${⊢}{W}=\left(\iota {b}\in {T}|{H}\left({X}\right)\in {b}\right)$
16 cvmlift3lem7.7 ${⊢}{\phi }\to {K}{↾}_{𝑡}{M}\in \mathrm{PConn}$
17 cvmlift3lem7.4 ${⊢}{\phi }\to {V}\in {K}$
18 cvmlift3lem7.5 ${⊢}{\phi }\to {V}\subseteq {M}$
19 cvmlift3lem7.6 ${⊢}{\phi }\to {X}\in {V}$
20 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 ${⊢}{\phi }\to {H}:{Y}⟶{B}$
21 1 2 3 4 5 6 7 8 9 10 cvmlift3lem5 ${⊢}{\phi }\to {F}\circ {H}={G}$
22 21 7 eqeltrd ${⊢}{\phi }\to {F}\circ {H}\in \left({K}\mathrm{Cn}{J}\right)$
23 sconntop ${⊢}{K}\in \mathrm{SConn}\to {K}\in \mathrm{Top}$
24 4 23 syl ${⊢}{\phi }\to {K}\in \mathrm{Top}$
25 cnvimass ${⊢}{{G}}^{-1}\left[{A}\right]\subseteq \mathrm{dom}{G}$
26 eqid ${⊢}\bigcup {J}=\bigcup {J}$
27 2 26 cnf ${⊢}{G}\in \left({K}\mathrm{Cn}{J}\right)\to {G}:{Y}⟶\bigcup {J}$
28 fdm ${⊢}{G}:{Y}⟶\bigcup {J}\to \mathrm{dom}{G}={Y}$
29 7 27 28 3syl ${⊢}{\phi }\to \mathrm{dom}{G}={Y}$
30 25 29 sseqtrid ${⊢}{\phi }\to {{G}}^{-1}\left[{A}\right]\subseteq {Y}$
31 14 30 sstrd ${⊢}{\phi }\to {M}\subseteq {Y}$
32 18 19 sseldd ${⊢}{\phi }\to {X}\in {M}$
33 31 32 sseldd ${⊢}{\phi }\to {X}\in {Y}$
34 20 33 ffvelrnd ${⊢}{\phi }\to {H}\left({X}\right)\in {B}$
35 fvco3 ${⊢}\left({H}:{Y}⟶{B}\wedge {X}\in {Y}\right)\to \left({F}\circ {H}\right)\left({X}\right)={F}\left({H}\left({X}\right)\right)$
36 20 33 35 syl2anc ${⊢}{\phi }\to \left({F}\circ {H}\right)\left({X}\right)={F}\left({H}\left({X}\right)\right)$
37 21 fveq1d ${⊢}{\phi }\to \left({F}\circ {H}\right)\left({X}\right)={G}\left({X}\right)$
38 36 37 eqtr3d ${⊢}{\phi }\to {F}\left({H}\left({X}\right)\right)={G}\left({X}\right)$
39 38 12 eqeltrd ${⊢}{\phi }\to {F}\left({H}\left({X}\right)\right)\in {A}$
40 11 1 15 cvmsiota ${⊢}\left({F}\in \left({C}\mathrm{CovMap}{J}\right)\wedge \left({T}\in {S}\left({A}\right)\wedge {H}\left({X}\right)\in {B}\wedge {F}\left({H}\left({X}\right)\right)\in {A}\right)\right)\to \left({W}\in {T}\wedge {H}\left({X}\right)\in {W}\right)$
41 3 13 34 39 40 syl13anc ${⊢}{\phi }\to \left({W}\in {T}\wedge {H}\left({X}\right)\in {W}\right)$
42 eqid ${⊢}{H}\left({X}\right)={H}\left({X}\right)$
43 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 ${⊢}\left({\phi }\wedge {X}\in {Y}\right)\to \left({H}\left({X}\right)={H}\left({X}\right)↔\exists {f}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={O}\wedge {f}\left(1\right)={X}\wedge \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\right)$
44 42 43 mpbii ${⊢}\left({\phi }\wedge {X}\in {Y}\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={O}\wedge {f}\left(1\right)={X}\wedge \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)$
45 33 44 mpdan ${⊢}{\phi }\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={O}\wedge {f}\left(1\right)={X}\wedge \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)$
46 45 adantr ${⊢}\left({\phi }\wedge {y}\in {M}\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={O}\wedge {f}\left(1\right)={X}\wedge \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)$
47 fveq1 ${⊢}{f}={h}\to {f}\left(0\right)={h}\left(0\right)$
48 47 eqeq1d ${⊢}{f}={h}\to \left({f}\left(0\right)={O}↔{h}\left(0\right)={O}\right)$
49 fveq1 ${⊢}{f}={h}\to {f}\left(1\right)={h}\left(1\right)$
50 49 eqeq1d ${⊢}{f}={h}\to \left({f}\left(1\right)={X}↔{h}\left(1\right)={X}\right)$
51 coeq2 ${⊢}{f}={h}\to {G}\circ {f}={G}\circ {h}$
52 51 eqeq2d ${⊢}{f}={h}\to \left({F}\circ {g}={G}\circ {f}↔{F}\circ {g}={G}\circ {h}\right)$
53 52 anbi1d ${⊢}{f}={h}\to \left(\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)↔\left({F}\circ {g}={G}\circ {h}\wedge {g}\left(0\right)={P}\right)\right)$
54 53 riotabidv ${⊢}{f}={h}\to \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)=\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {h}\wedge {g}\left(0\right)={P}\right)\right)$
55 coeq2 ${⊢}{a}={g}\to {F}\circ {a}={F}\circ {g}$
56 55 eqeq1d ${⊢}{a}={g}\to \left({F}\circ {a}={G}\circ {h}↔{F}\circ {g}={G}\circ {h}\right)$
57 fveq1 ${⊢}{a}={g}\to {a}\left(0\right)={g}\left(0\right)$
58 57 eqeq1d ${⊢}{a}={g}\to \left({a}\left(0\right)={P}↔{g}\left(0\right)={P}\right)$
59 56 58 anbi12d ${⊢}{a}={g}\to \left(\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)↔\left({F}\circ {g}={G}\circ {h}\wedge {g}\left(0\right)={P}\right)\right)$
60 59 cbvriotav ${⊢}\left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)=\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {h}\wedge {g}\left(0\right)={P}\right)\right)$
61 54 60 syl6eqr ${⊢}{f}={h}\to \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)=\left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)$
62 61 fveq1d ${⊢}{f}={h}\to \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)=\left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)$
63 62 eqeq1d ${⊢}{f}={h}\to \left(\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)↔\left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)$
64 48 50 63 3anbi123d ${⊢}{f}={h}\to \left(\left({f}\left(0\right)={O}\wedge {f}\left(1\right)={X}\wedge \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)↔\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\right)$
65 64 cbvrexv ${⊢}\exists {f}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={O}\wedge {f}\left(1\right)={X}\wedge \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {f}\wedge {g}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)↔\exists {h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)$
66 46 65 sylib ${⊢}\left({\phi }\wedge {y}\in {M}\right)\to \exists {h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)$
67 16 adantr ${⊢}\left({\phi }\wedge {y}\in {M}\right)\to {K}{↾}_{𝑡}{M}\in \mathrm{PConn}$
68 2 restuni ${⊢}\left({K}\in \mathrm{Top}\wedge {M}\subseteq {Y}\right)\to {M}=\bigcup \left({K}{↾}_{𝑡}{M}\right)$
69 24 31 68 syl2anc ${⊢}{\phi }\to {M}=\bigcup \left({K}{↾}_{𝑡}{M}\right)$
70 32 69 eleqtrd ${⊢}{\phi }\to {X}\in \bigcup \left({K}{↾}_{𝑡}{M}\right)$
71 70 adantr ${⊢}\left({\phi }\wedge {y}\in {M}\right)\to {X}\in \bigcup \left({K}{↾}_{𝑡}{M}\right)$
72 69 eleq2d ${⊢}{\phi }\to \left({y}\in {M}↔{y}\in \bigcup \left({K}{↾}_{𝑡}{M}\right)\right)$
73 72 biimpa ${⊢}\left({\phi }\wedge {y}\in {M}\right)\to {y}\in \bigcup \left({K}{↾}_{𝑡}{M}\right)$
74 eqid ${⊢}\bigcup \left({K}{↾}_{𝑡}{M}\right)=\bigcup \left({K}{↾}_{𝑡}{M}\right)$
75 74 pconncn ${⊢}\left({K}{↾}_{𝑡}{M}\in \mathrm{PConn}\wedge {X}\in \bigcup \left({K}{↾}_{𝑡}{M}\right)\wedge {y}\in \bigcup \left({K}{↾}_{𝑡}{M}\right)\right)\to \exists {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\phantom{\rule{.4em}{0ex}}\left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)$
76 67 71 73 75 syl3anc ${⊢}\left({\phi }\wedge {y}\in {M}\right)\to \exists {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\phantom{\rule{.4em}{0ex}}\left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)$
77 reeanv ${⊢}\exists {h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)↔\left(\exists {h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \exists {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\phantom{\rule{.4em}{0ex}}\left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)$
78 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
79 4 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {K}\in \mathrm{SConn}$
80 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {K}\in N-Locally\mathrm{PConn}$
81 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {O}\in {Y}$
82 7 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {G}\in \left({K}\mathrm{Cn}{J}\right)$
83 8 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {P}\in {B}$
84 9 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {F}\left({P}\right)={G}\left({O}\right)$
85 12 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {G}\left({X}\right)\in {A}$
86 13 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {T}\in {S}\left({A}\right)$
87 14 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {M}\subseteq {{G}}^{-1}\left[{A}\right]$
88 32 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {X}\in {M}$
89 simpllr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {y}\in {M}$
90 simplrl ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)$
91 simprl ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to \left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)$
92 simplrr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)$
93 simprr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)$
94 55 eqeq1d ${⊢}{a}={g}\to \left({F}\circ {a}={G}\circ {n}↔{F}\circ {g}={G}\circ {n}\right)$
95 57 eqeq1d ${⊢}{a}={g}\to \left({a}\left(0\right)={H}\left({X}\right)↔{g}\left(0\right)={H}\left({X}\right)\right)$
96 94 95 anbi12d ${⊢}{a}={g}\to \left(\left({F}\circ {a}={G}\circ {n}\wedge {a}\left(0\right)={H}\left({X}\right)\right)↔\left({F}\circ {g}={G}\circ {n}\wedge {g}\left(0\right)={H}\left({X}\right)\right)\right)$
97 96 cbvriotav ${⊢}\left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {n}\wedge {a}\left(0\right)={H}\left({X}\right)\right)\right)=\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}={G}\circ {n}\wedge {g}\left(0\right)={H}\left({X}\right)\right)\right)$
98 1 2 78 79 80 81 82 83 84 10 11 85 86 87 15 88 89 90 60 91 92 93 97 cvmlift3lem6 ${⊢}\left(\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\wedge \left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\right)\to {H}\left({y}\right)\in {W}$
99 98 ex ${⊢}\left(\left({\phi }\wedge {y}\in {M}\right)\wedge \left({h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\wedge {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\right)\right)\to \left(\left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\to {H}\left({y}\right)\in {W}\right)$
100 99 rexlimdvva ${⊢}\left({\phi }\wedge {y}\in {M}\right)\to \left(\exists {h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\to {H}\left({y}\right)\in {W}\right)$
101 77 100 syl5bir ${⊢}\left({\phi }\wedge {y}\in {M}\right)\to \left(\left(\exists {h}\in \left(\mathrm{II}\mathrm{Cn}{K}\right)\phantom{\rule{.4em}{0ex}}\left({h}\left(0\right)={O}\wedge {h}\left(1\right)={X}\wedge \left(\iota {a}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {a}={G}\circ {h}\wedge {a}\left(0\right)={P}\right)\right)\left(1\right)={H}\left({X}\right)\right)\wedge \exists {n}\in \left(\mathrm{II}\mathrm{Cn}\left({K}{↾}_{𝑡}{M}\right)\right)\phantom{\rule{.4em}{0ex}}\left({n}\left(0\right)={X}\wedge {n}\left(1\right)={y}\right)\right)\to {H}\left({y}\right)\in {W}\right)$
102 66 76 101 mp2and ${⊢}\left({\phi }\wedge {y}\in {M}\right)\to {H}\left({y}\right)\in {W}$
103 102 ralrimiva ${⊢}{\phi }\to \forall {y}\in {M}\phantom{\rule{.4em}{0ex}}{H}\left({y}\right)\in {W}$
104 20 ffund ${⊢}{\phi }\to \mathrm{Fun}{H}$
105 20 fdmd ${⊢}{\phi }\to \mathrm{dom}{H}={Y}$
106 31 105 sseqtrrd ${⊢}{\phi }\to {M}\subseteq \mathrm{dom}{H}$
107 funimass4 ${⊢}\left(\mathrm{Fun}{H}\wedge {M}\subseteq \mathrm{dom}{H}\right)\to \left({H}\left[{M}\right]\subseteq {W}↔\forall {y}\in {M}\phantom{\rule{.4em}{0ex}}{H}\left({y}\right)\in {W}\right)$
108 104 106 107 syl2anc ${⊢}{\phi }\to \left({H}\left[{M}\right]\subseteq {W}↔\forall {y}\in {M}\phantom{\rule{.4em}{0ex}}{H}\left({y}\right)\in {W}\right)$
109 103 108 mpbird ${⊢}{\phi }\to {H}\left[{M}\right]\subseteq {W}$
110 1 2 11 3 20 22 24 33 13 41 31 109 cvmlift2lem9a ${⊢}{\phi }\to {{H}↾}_{{M}}\in \left(\left({K}{↾}_{𝑡}{M}\right)\mathrm{Cn}{C}\right)$
111 74 cncnpi ${⊢}\left({{H}↾}_{{M}}\in \left(\left({K}{↾}_{𝑡}{M}\right)\mathrm{Cn}{C}\right)\wedge {X}\in \bigcup \left({K}{↾}_{𝑡}{M}\right)\right)\to {{H}↾}_{{M}}\in \left(\left({K}{↾}_{𝑡}{M}\right)\mathrm{CnP}{C}\right)\left({X}\right)$
112 110 70 111 syl2anc ${⊢}{\phi }\to {{H}↾}_{{M}}\in \left(\left({K}{↾}_{𝑡}{M}\right)\mathrm{CnP}{C}\right)\left({X}\right)$
113 2 ssntr ${⊢}\left(\left({K}\in \mathrm{Top}\wedge {M}\subseteq {Y}\right)\wedge \left({V}\in {K}\wedge {V}\subseteq {M}\right)\right)\to {V}\subseteq \mathrm{int}\left({K}\right)\left({M}\right)$
114 24 31 17 18 113 syl22anc ${⊢}{\phi }\to {V}\subseteq \mathrm{int}\left({K}\right)\left({M}\right)$
115 114 19 sseldd ${⊢}{\phi }\to {X}\in \mathrm{int}\left({K}\right)\left({M}\right)$
116 2 1 cnprest ${⊢}\left(\left({K}\in \mathrm{Top}\wedge {M}\subseteq {Y}\right)\wedge \left({X}\in \mathrm{int}\left({K}\right)\left({M}\right)\wedge {H}:{Y}⟶{B}\right)\right)\to \left({H}\in \left({K}\mathrm{CnP}{C}\right)\left({X}\right)↔{{H}↾}_{{M}}\in \left(\left({K}{↾}_{𝑡}{M}\right)\mathrm{CnP}{C}\right)\left({X}\right)\right)$
117 24 31 115 20 116 syl22anc ${⊢}{\phi }\to \left({H}\in \left({K}\mathrm{CnP}{C}\right)\left({X}\right)↔{{H}↾}_{{M}}\in \left(\left({K}{↾}_{𝑡}{M}\right)\mathrm{CnP}{C}\right)\left({X}\right)\right)$
118 112 117 mpbird ${⊢}{\phi }\to {H}\in \left({K}\mathrm{CnP}{C}\right)\left({X}\right)$