Theorem cvmliftlem4

Description: Lemma for cvmlift . The function Q will be our lifted path, defined piecewise on each section [ ( M - 1 ) / N , M / N ] for M e. ( 1 ... N ) . For M = 0 , it is a "seed" value which makes the rest of the recursion work, a singleton function mapping 0 to P . (Contributed by Mario Carneiro, 15-Feb-2015)

	Ref	Expression
Hypotheses	cvmliftlem.1	$$⊢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 u\in s\left(\forall v\in \left(s\setminus \left\{u\right\}\right)u\cap v=\varnothing \wedge {F\upharpoonright }_u\in \left(\left(C{\upharpoonright }_{𝑡}u\right)\mathrm{Homeo}\left(J{\upharpoonright }_{𝑡}k\right)\right)\right)\right)\right\}\right)$$
	cvmliftlem.b	$$⊢B=\bigcup C$$
	cvmliftlem.x	$$⊢X=\bigcup J$$
	cvmliftlem.f	$$⊢\phi \to F\in \left(C\mathrm{CovMap}J\right)$$
	cvmliftlem.g	$$⊢\phi \to G\in \left(\mathrm{II}\mathrm{Cn}J\right)$$
	cvmliftlem.p	$$⊢\phi \to P\in B$$
	cvmliftlem.e	$$⊢\phi \to F\left(P\right)=G\left(0\right)$$
	cvmliftlem.n	$$⊢\phi \to N\in \mathbb{N}$$
	cvmliftlem.t	$$⊢\phi \to T:\left(1\dots N\right)⟶\bigcup _{j\in J}\left(\left\{j\right\}\times S\left(j\right)\right)$$
	cvmliftlem.a	$$⊢\phi \to \forall k\in \left(1\dots N\right)G\left[\left[\frac{k-1}{N},\frac{k}{N}\right]\right]\subseteq 1^{st}\left(T\left(k\right)\right)$$
	cvmliftlem.l	$$⊢L=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	cvmliftlem.q	$$⊢Q=seq0\left(\left(x\in \mathrm{V},m\in \mathbb{N}⟼\left(z\in \left[\frac{m-1}{N},\frac{m}{N}\right]⟼{\left({F\upharpoonright }_{\left(\iota b\in 2^{nd}\left(T\left(m\right)\right)|x\left(\frac{m-1}{N}\right)\in b\right)}\right)}^{-1}\left(G\left(z\right)\right)\right)\right),\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\right)$$
Assertion	cvmliftlem4	$$⊢Q\left(0\right)=\left\{⟨0,P⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cvmliftlem.1	$$⊢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 u\in s\left(\forall v\in \left(s\setminus \left\{u\right\}\right)u\cap v=\varnothing \wedge {F\upharpoonright }_u\in \left(\left(C{\upharpoonright }_{𝑡}u\right)\mathrm{Homeo}\left(J{\upharpoonright }_{𝑡}k\right)\right)\right)\right)\right\}\right)$$
2		cvmliftlem.b	$$⊢B=\bigcup C$$
3		cvmliftlem.x	$$⊢X=\bigcup J$$
4		cvmliftlem.f	$$⊢\phi \to F\in \left(C\mathrm{CovMap}J\right)$$
5		cvmliftlem.g	$$⊢\phi \to G\in \left(\mathrm{II}\mathrm{Cn}J\right)$$
6		cvmliftlem.p	$$⊢\phi \to P\in B$$
7		cvmliftlem.e	$$⊢\phi \to F\left(P\right)=G\left(0\right)$$
8		cvmliftlem.n	$$⊢\phi \to N\in \mathbb{N}$$
9		cvmliftlem.t	$$⊢\phi \to T:\left(1\dots N\right)⟶\bigcup _{j\in J}\left(\left\{j\right\}\times S\left(j\right)\right)$$
10		cvmliftlem.a	$$⊢\phi \to \forall k\in \left(1\dots N\right)G\left[\left[\frac{k-1}{N},\frac{k}{N}\right]\right]\subseteq 1^{st}\left(T\left(k\right)\right)$$
11		cvmliftlem.l	$$⊢L=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
12		cvmliftlem.q	$$⊢Q=seq0\left(\left(x\in \mathrm{V},m\in \mathbb{N}⟼\left(z\in \left[\frac{m-1}{N},\frac{m}{N}\right]⟼{\left({F\upharpoonright }_{\left(\iota b\in 2^{nd}\left(T\left(m\right)\right)|x\left(\frac{m-1}{N}\right)\in b\right)}\right)}^{-1}\left(G\left(z\right)\right)\right)\right),\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\right)$$
13	12	fveq1i	$$⊢Q\left(0\right)=seq0\left(\left(x\in \mathrm{V},m\in \mathbb{N}⟼\left(z\in \left[\frac{m-1}{N},\frac{m}{N}\right]⟼{\left({F\upharpoonright }_{\left(\iota b\in 2^{nd}\left(T\left(m\right)\right)|x\left(\frac{m-1}{N}\right)\in b\right)}\right)}^{-1}\left(G\left(z\right)\right)\right)\right),\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\right)\left(0\right)$$
14		0z	$$⊢0\in \mathbb{Z}$$
15		seq1	$$⊢0\in \mathbb{Z}\to seq0\left(\left(x\in \mathrm{V},m\in \mathbb{N}⟼\left(z\in \left[\frac{m-1}{N},\frac{m}{N}\right]⟼{\left({F\upharpoonright }_{\left(\iota b\in 2^{nd}\left(T\left(m\right)\right)|x\left(\frac{m-1}{N}\right)\in b\right)}\right)}^{-1}\left(G\left(z\right)\right)\right)\right),\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\right)\left(0\right)=\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\left(0\right)$$
16	14 15	ax-mp	$$⊢seq0\left(\left(x\in \mathrm{V},m\in \mathbb{N}⟼\left(z\in \left[\frac{m-1}{N},\frac{m}{N}\right]⟼{\left({F\upharpoonright }_{\left(\iota b\in 2^{nd}\left(T\left(m\right)\right)|x\left(\frac{m-1}{N}\right)\in b\right)}\right)}^{-1}\left(G\left(z\right)\right)\right)\right),\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\right)\left(0\right)=\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\left(0\right)$$
17	13 16	eqtri	$$⊢Q\left(0\right)=\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\left(0\right)$$
18		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)Fn\mathbb{N}$$
19		c0ex	$$⊢0\in \mathrm{V}$$
20		snex	$$⊢\left\{⟨0,P⟩\right\}\in \mathrm{V}$$
21	19 20	fnsn	$$⊢\left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}Fn\left\{0\right\}$$
22		0nnn	$$⊢\neg 0\in \mathbb{N}$$
23		disjsn	$$⊢\mathbb{N}\cap \left\{0\right\}=\varnothing \leftrightarrow \neg 0\in \mathbb{N}$$
24	22 23	mpbir	$$⊢\mathbb{N}\cap \left\{0\right\}=\varnothing$$
25	19	snid	$$⊢0\in \left\{0\right\}$$
26	24 25	pm3.2i	$$⊢\left(\mathbb{N}\cap \left\{0\right\}=\varnothing \wedge 0\in \left\{0\right\}\right)$$
27		fvun2	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)Fn\mathbb{N}\wedge \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}Fn\left\{0\right\}\wedge \left(\mathbb{N}\cap \left\{0\right\}=\varnothing \wedge 0\in \left\{0\right\}\right)\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\left(0\right)=\left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\left(0\right)$$
28	18 21 26 27	mp3an	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\cup \left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\right)\left(0\right)=\left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\left(0\right)$$
29	17 28	eqtri	$$⊢Q\left(0\right)=\left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\left(0\right)$$
30	19 20	fvsn	$$⊢\left\{⟨0,\left\{⟨0,P⟩\right\}⟩\right\}\left(0\right)=\left\{⟨0,P⟩\right\}$$
31	29 30	eqtri	$$⊢Q\left(0\right)=\left\{⟨0,P⟩\right\}$$