cvmliftlem15

Description: Lemma for cvmlift . Discharge the assumptions of cvmliftlem14 . The set of all open subsets u of the unit interval such that G " u is contained in an even covering of some open set in J is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii , there is a subdivision of the closed unit interval into N equal parts such that each part is entirely contained within one such open set of J . Then using finite choice ac6sfi to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 . (Contributed by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypotheses	cvmliftlem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	cvmliftlem.b	$⊢ B = ⋃ C$
	cvmliftlem.x	$⊢ X = ⋃ J$
	cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
	cvmliftlem.p	$⊢ φ \to P \in B$
	cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
Assertion	cvmliftlem15	$⊢ φ \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P)$

Proof

Step	Hyp	Ref	Expression
1		cvmliftlem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		cvmliftlem.b	$⊢ B = ⋃ C$
3		cvmliftlem.x	$⊢ X = ⋃ J$
4		cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
5		cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
6		cvmliftlem.p	$⊢ φ \to P \in B$
7		cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
8		ssrab2	$⊢ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} \subseteq II$
9	5	ad2antrr	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to G \in (II Cn J)$
10		simprl	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to j \in J$
11		cnima	$⊢ (G \in (II Cn J) \land j \in J) \to G^{-1} [j] \in II$
12	9 10 11	syl2anc	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to G^{-1} [j] \in II$
13		simplr	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to x \in [0, 1]$
14		simprrl	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to G (x) \in j$
15		iiuni	$⊢ [0, 1] = ⋃ II$
16	15 3	cnf	$⊢ G \in (II Cn J) \to G : [0, 1] ⟶ X$
17	5 16	syl	$⊢ φ \to G : [0, 1] ⟶ X$
18	17	ad2antrr	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to G : [0, 1] ⟶ X$
19		ffn	$⊢ G : [0, 1] ⟶ X \to G Fn [0, 1]$
20		elpreima	$⊢ G Fn [0, 1] \to (x \in G^{-1} [j] \leftrightarrow (x \in [0, 1] \land G (x) \in j))$
21	18 19 20	3syl	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to (x \in G^{-1} [j] \leftrightarrow (x \in [0, 1] \land G (x) \in j))$
22	13 14 21	mpbir2and	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to x \in G^{-1} [j]$
23		simprrr	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to S (j) \neq \emptyset$
24		ffun	$⊢ G : [0, 1] ⟶ X \to Fun G$
25		funimacnv	$⊢ Fun G \to G [G^{-1} [j]] = j \cap ran G$
26	18 24 25	3syl	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to G [G^{-1} [j]] = j \cap ran G$
27		inss1	$⊢ j \cap ran G \subseteq j$
28	26 27	eqsstrdi	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to G [G^{-1} [j]] \subseteq j$
29	28	ralrimivw	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to \forall s \in S (j) G [G^{-1} [j]] \subseteq j$
30		r19.2z	$⊢ (S (j) \neq \emptyset \land \forall s \in S (j) G [G^{-1} [j]] \subseteq j) \to \exists s \in S (j) G [G^{-1} [j]] \subseteq j$
31	23 29 30	syl2anc	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to \exists s \in S (j) G [G^{-1} [j]] \subseteq j$
32		eleq2	$⊢ u = G^{-1} [j] \to (x \in u \leftrightarrow x \in G^{-1} [j])$
33		imaeq2	$⊢ u = G^{-1} [j] \to G [u] = G [G^{-1} [j]]$
34	33	sseq1d	$⊢ u = G^{-1} [j] \to (G [u] \subseteq j \leftrightarrow G [G^{-1} [j]] \subseteq j)$
35	34	rexbidv	$⊢ u = G^{-1} [j] \to (\exists s \in S (j) G [u] \subseteq j \leftrightarrow \exists s \in S (j) G [G^{-1} [j]] \subseteq j)$
36	32 35	anbi12d	$⊢ u = G^{-1} [j] \to ((x \in u \land \exists s \in S (j) G [u] \subseteq j) \leftrightarrow (x \in G^{-1} [j] \land \exists s \in S (j) G [G^{-1} [j]] \subseteq j))$
37	36	rspcev	$⊢ (G^{-1} [j] \in II \land (x \in G^{-1} [j] \land \exists s \in S (j) G [G^{-1} [j]] \subseteq j)) \to \exists u \in II (x \in u \land \exists s \in S (j) G [u] \subseteq j)$
38	12 22 31 37	syl12anc	$⊢ ((φ \land x \in [0, 1]) \land (j \in J \land (G (x) \in j \land S (j) \neq \emptyset))) \to \exists u \in II (x \in u \land \exists s \in S (j) G [u] \subseteq j)$
39	4	adantr	$⊢ (φ \land x \in [0, 1]) \to F \in (C CovMap J)$
40	17	ffvelcdmda	$⊢ (φ \land x \in [0, 1]) \to G (x) \in X$
41	1 3	cvmcov	$⊢ (F \in (C CovMap J) \land G (x) \in X) \to \exists j \in J (G (x) \in j \land S (j) \neq \emptyset)$
42	39 40 41	syl2anc	$⊢ (φ \land x \in [0, 1]) \to \exists j \in J (G (x) \in j \land S (j) \neq \emptyset)$
43	38 42	reximddv	$⊢ (φ \land x \in [0, 1]) \to \exists j \in J \exists u \in II (x \in u \land \exists s \in S (j) G [u] \subseteq j)$
44		r19.42v	$⊢ \exists j \in J (x \in u \land \exists s \in S (j) G [u] \subseteq j) \leftrightarrow (x \in u \land \exists j \in J \exists s \in S (j) G [u] \subseteq j)$
45	44	rexbii	$⊢ \exists u \in II \exists j \in J (x \in u \land \exists s \in S (j) G [u] \subseteq j) \leftrightarrow \exists u \in II (x \in u \land \exists j \in J \exists s \in S (j) G [u] \subseteq j)$
46		rexcom	$⊢ \exists j \in J \exists u \in II (x \in u \land \exists s \in S (j) G [u] \subseteq j) \leftrightarrow \exists u \in II \exists j \in J (x \in u \land \exists s \in S (j) G [u] \subseteq j)$
47		elunirab	$⊢ x \in ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} \leftrightarrow \exists u \in II (x \in u \land \exists j \in J \exists s \in S (j) G [u] \subseteq j)$
48	45 46 47	3bitr4i	$⊢ \exists j \in J \exists u \in II (x \in u \land \exists s \in S (j) G [u] \subseteq j) \leftrightarrow x \in ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\}$
49	43 48	sylib	$⊢ (φ \land x \in [0, 1]) \to x \in ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\}$
50	49	ex	$⊢ φ \to (x \in [0, 1] \to x \in ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\})$
51	50	ssrdv	$⊢ φ \to [0, 1] \subseteq ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\}$
52		uniss	$⊢ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} \subseteq II \to ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} \subseteq ⋃ II$
53	8 52	mp1i	$⊢ φ \to ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} \subseteq ⋃ II$
54	53 15	sseqtrrdi	$⊢ φ \to ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} \subseteq [0, 1]$
55	51 54	eqssd	$⊢ φ \to [0, 1] = ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\}$
56		lebnumii	$⊢ (\{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} \subseteq II \land [0, 1] = ⋃ \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\}) \to \exists n \in ℕ \forall k \in (1 \dots n) \exists v \in \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v$
57	8 55 56	sylancr	$⊢ φ \to \exists n \in ℕ \forall k \in (1 \dots n) \exists v \in \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v$
58		fzfi	$⊢ (1 \dots n) \in Fin$
59		imaeq2	$⊢ u = v \to G [u] = G [v]$
60	59	sseq1d	$⊢ u = v \to (G [u] \subseteq j \leftrightarrow G [v] \subseteq j)$
61	60	2rexbidv	$⊢ u = v \to (\exists j \in J \exists s \in S (j) G [u] \subseteq j \leftrightarrow \exists j \in J \exists s \in S (j) G [v] \subseteq j)$
62	61	rexrab	$⊢ \exists v \in \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \leftrightarrow \exists v \in II (\exists j \in J \exists s \in S (j) G [v] \subseteq j \land [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v)$
63		vex	$⊢ j \in V$
64		vex	$⊢ s \in V$
65	63 64	op1std	$⊢ u = ⟨j, s⟩ \to 1^{st} (u) = j$
66	65	sseq2d	$⊢ u = ⟨j, s⟩ \to (G [v] \subseteq 1^{st} (u) \leftrightarrow G [v] \subseteq j)$
67	66	rexiunxp	$⊢ \exists u \in ⋃_{j \in J} (\{j\} \times S (j)) G [v] \subseteq 1^{st} (u) \leftrightarrow \exists j \in J \exists s \in S (j) G [v] \subseteq j$
68		imass2	$⊢ [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \to G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq G [v]$
69		sstr2	$⊢ G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq G [v] \to (G [v] \subseteq 1^{st} (u) \to G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u))$
70	68 69	syl	$⊢ [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \to (G [v] \subseteq 1^{st} (u) \to G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u))$
71	70	reximdv	$⊢ [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \to (\exists u \in ⋃_{j \in J} (\{j\} \times S (j)) G [v] \subseteq 1^{st} (u) \to \exists u \in ⋃_{j \in J} (\{j\} \times S (j)) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u))$
72	67 71	biimtrrid	$⊢ [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \to (\exists j \in J \exists s \in S (j) G [v] \subseteq j \to \exists u \in ⋃_{j \in J} (\{j\} \times S (j)) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u))$
73	72	impcom	$⊢ (\exists j \in J \exists s \in S (j) G [v] \subseteq j \land [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v) \to \exists u \in ⋃_{j \in J} (\{j\} \times S (j)) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u)$
74	73	rexlimivw	$⊢ \exists v \in II (\exists j \in J \exists s \in S (j) G [v] \subseteq j \land [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v) \to \exists u \in ⋃_{j \in J} (\{j\} \times S (j)) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u)$
75	62 74	sylbi	$⊢ \exists v \in \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \to \exists u \in ⋃_{j \in J} (\{j\} \times S (j)) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u)$
76	75	ralimi	$⊢ \forall k \in (1 \dots n) \exists v \in \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \to \forall k \in (1 \dots n) \exists u \in ⋃_{j \in J} (\{j\} \times S (j)) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u)$
77		fveq2	$⊢ u = g (k) \to 1^{st} (u) = 1^{st} (g (k))$
78	77	sseq2d	$⊢ u = g (k) \to (G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u) \leftrightarrow G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))$
79	78	ac6sfi	$⊢ ((1 \dots n) \in Fin \land \forall k \in (1 \dots n) \exists u \in ⋃_{j \in J} (\{j\} \times S (j)) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (u)) \to \exists g (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))$
80	58 76 79	sylancr	$⊢ \forall k \in (1 \dots n) \exists v \in \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \to \exists g (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))$
81	4	ad2antrr	$⊢ ((φ \land n \in ℕ) \land (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))) \to F \in (C CovMap J)$
82	5	ad2antrr	$⊢ ((φ \land n \in ℕ) \land (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))) \to G \in (II Cn J)$
83	6	ad2antrr	$⊢ ((φ \land n \in ℕ) \land (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))) \to P \in B$
84	7	ad2antrr	$⊢ ((φ \land n \in ℕ) \land (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))) \to F (P) = G (0)$
85		simplr	$⊢ ((φ \land n \in ℕ) \land (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))) \to n \in ℕ$
86		simprl	$⊢ ((φ \land n \in ℕ) \land (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))) \to g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
87		sneq	$⊢ j = a \to \{j\} = \{a\}$
88		fveq2	$⊢ j = a \to S (j) = S (a)$
89	87 88	xpeq12d	$⊢ j = a \to \{j\} \times S (j) = \{a\} \times S (a)$
90	89	cbviunv	$⊢ ⋃_{j \in J} (\{j\} \times S (j)) = ⋃_{a \in J} (\{a\} \times S (a))$
91		feq3	$⊢ ⋃_{j \in J} (\{j\} \times S (j)) = ⋃_{a \in J} (\{a\} \times S (a)) \to (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \leftrightarrow g : (1 \dots n) ⟶ ⋃_{a \in J} (\{a\} \times S (a)))$
92	90 91	ax-mp	$⊢ g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \leftrightarrow g : (1 \dots n) ⟶ ⋃_{a \in J} (\{a\} \times S (a))$
93	86 92	sylib	$⊢ ((φ \land n \in ℕ) \land (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))) \to g : (1 \dots n) ⟶ ⋃_{a \in J} (\{a\} \times S (a))$
94		simprr	$⊢ ((φ \land n \in ℕ) \land (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))) \to \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k))$
95		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
96		2fveq3	$⊢ t = z \to {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (t)) = {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (z))$
97	96	cbvmptv	$⊢ (t \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (t))) = (z \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (z)))$
98		eleq2	$⊢ c = b \to (y (\frac{w - 1}{n}) \in c \leftrightarrow y (\frac{w - 1}{n}) \in b)$
99	98	cbvriotavw	$⊢ (ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c) = (ι b \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in b)$
100		fveq1	$⊢ y = x \to y (\frac{w - 1}{n}) = x (\frac{w - 1}{n})$
101	100	eleq1d	$⊢ y = x \to (y (\frac{w - 1}{n}) \in b \leftrightarrow x (\frac{w - 1}{n}) \in b)$
102	101	riotabidv	$⊢ y = x \to (ι b \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in b) = (ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)$
103	99 102	eqtrid	$⊢ y = x \to (ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c) = (ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)$
104	103	reseq2d	$⊢ y = x \to {F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)} = {F ↾}_{(ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)}$
105	104	cnveqd	$⊢ y = x \to {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} = {({F ↾}_{(ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)})}^{-1}$
106	105	fveq1d	$⊢ y = x \to {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (z)) = {({F ↾}_{(ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)})}^{-1} (G (z))$
107	106	mpteq2dv	$⊢ y = x \to (z \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (z))) = (z \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)})}^{-1} (G (z)))$
108	97 107	eqtrid	$⊢ y = x \to (t \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (t))) = (z \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)})}^{-1} (G (z)))$
109		oveq1	$⊢ w = m \to w - 1 = m - 1$
110	109	oveq1d	$⊢ w = m \to \frac{w - 1}{n} = \frac{m - 1}{n}$
111		oveq1	$⊢ w = m \to \frac{w}{n} = \frac{m}{n}$
112	110 111	oveq12d	$⊢ w = m \to [\frac{w - 1}{n}, \frac{w}{n}] = [\frac{m - 1}{n}, \frac{m}{n}]$
113		2fveq3	$⊢ w = m \to 2^{nd} (g (w)) = 2^{nd} (g (m))$
114	110	fveq2d	$⊢ w = m \to x (\frac{w - 1}{n}) = x (\frac{m - 1}{n})$
115	114	eleq1d	$⊢ w = m \to (x (\frac{w - 1}{n}) \in b \leftrightarrow x (\frac{m - 1}{n}) \in b)$
116	113 115	riotaeqbidv	$⊢ w = m \to (ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b) = (ι b \in 2^{nd} (g (m)) \| x (\frac{m - 1}{n}) \in b)$
117	116	reseq2d	$⊢ w = m \to {F ↾}_{(ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)} = {F ↾}_{(ι b \in 2^{nd} (g (m)) \| x (\frac{m - 1}{n}) \in b)}$
118	117	cnveqd	$⊢ w = m \to {({F ↾}_{(ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)})}^{-1} = {({F ↾}_{(ι b \in 2^{nd} (g (m)) \| x (\frac{m - 1}{n}) \in b)})}^{-1}$
119	118	fveq1d	$⊢ w = m \to {({F ↾}_{(ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)})}^{-1} (G (z)) = {({F ↾}_{(ι b \in 2^{nd} (g (m)) \| x (\frac{m - 1}{n}) \in b)})}^{-1} (G (z))$
120	112 119	mpteq12dv	$⊢ w = m \to (z \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (g (w)) \| x (\frac{w - 1}{n}) \in b)})}^{-1} (G (z))) = (z \in [\frac{m - 1}{n}, \frac{m}{n}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (g (m)) \| x (\frac{m - 1}{n}) \in b)})}^{-1} (G (z)))$
121	108 120	cbvmpov	$⊢ (y \in V, w \in ℕ ⟼ (t \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (t)))) = (x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{n}, \frac{m}{n}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (g (m)) \| x (\frac{m - 1}{n}) \in b)})}^{-1} (G (z))))$
122		seqeq2	$⊢ (y \in V, w \in ℕ ⟼ (t \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (t)))) = (x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{n}, \frac{m}{n}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (g (m)) \| x (\frac{m - 1}{n}) \in b)})}^{-1} (G (z)))) \to seq 0 ((y \in V, w \in ℕ ⟼ (t \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (t)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\})) = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{n}, \frac{m}{n}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (g (m)) \| x (\frac{m - 1}{n}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
123	121 122	ax-mp	$⊢ seq 0 ((y \in V, w \in ℕ ⟼ (t \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (t)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\})) = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{n}, \frac{m}{n}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (g (m)) \| x (\frac{m - 1}{n}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
124		eqid	$⊢ ⋃_{k = 1}^{n} seq 0 ((y \in V, w \in ℕ ⟼ (t \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (t)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\})) (k) = ⋃_{k = 1}^{n} seq 0 ((y \in V, w \in ℕ ⟼ (t \in [\frac{w - 1}{n}, \frac{w}{n}] ⟼ {({F ↾}_{(ι c \in 2^{nd} (g (w)) \| y (\frac{w - 1}{n}) \in c)})}^{-1} (G (t)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\})) (k)$
125	1 2 3 81 82 83 84 85 93 94 95 123 124	cvmliftlem14	$⊢ ((φ \land n \in ℕ) \land (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k)))) \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P)$
126	125	ex	$⊢ (φ \land n \in ℕ) \to ((g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k))) \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P))$
127	126	exlimdv	$⊢ (φ \land n \in ℕ) \to (\exists g (g : (1 \dots n) ⟶ ⋃_{j \in J} (\{j\} \times S (j)) \land \forall k \in (1 \dots n) G [[\frac{k - 1}{n}, \frac{k}{n}]] \subseteq 1^{st} (g (k))) \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P))$
128	80 127	syl5	$⊢ (φ \land n \in ℕ) \to (\forall k \in (1 \dots n) \exists v \in \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P))$
129	128	rexlimdva	$⊢ φ \to (\exists n \in ℕ \forall k \in (1 \dots n) \exists v \in \{u \in II \| \exists j \in J \exists s \in S (j) G [u] \subseteq j\} [\frac{k - 1}{n}, \frac{k}{n}] \subseteq v \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P))$
130	57 129	mpd	$⊢ φ \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P)$

Metamath Proof Explorer

Theorem cvmliftlem15

Proof