cvmliftlem14

Description: Lemma for cvmlift . Putting the results of cvmliftlem11 , cvmliftlem13 and cvmliftmo together, we have that K is a continuous function, satisfies F o. K = G and K ( 0 ) = P , and is equal to any other function which also has these properties, so it follows that K is the unique lift of G . (Contributed by Mario Carneiro, 16-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)$
	cvmliftlem.n	$⊢ φ \to N \in ℕ$
	cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
	cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
	cvmliftlem.l	$⊢ L = topGen (ran (.))$
	cvmliftlem.q	$⊢ Q = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
	cvmliftlem.k	$⊢ K = ⋃_{k = 1}^{N} Q (k)$
Assertion	cvmliftlem14	$⊢ φ \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		cvmliftlem.n	$⊢ φ \to N \in ℕ$
9		cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
10		cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
11		cvmliftlem.l	$⊢ L = topGen (ran (.))$
12		cvmliftlem.q	$⊢ Q = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
13		cvmliftlem.k	$⊢ K = ⋃_{k = 1}^{N} Q (k)$
14	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem11	$⊢ φ \to (K \in (II Cn C) \land F \circ K = G)$
15	14	simpld	$⊢ φ \to K \in (II Cn C)$
16	14	simprd	$⊢ φ \to F \circ K = G$
17	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem13	$⊢ φ \to K (0) = P$
18		coeq2	$⊢ f = K \to F \circ f = F \circ K$
19	18	eqeq1d	$⊢ f = K \to (F \circ f = G \leftrightarrow F \circ K = G)$
20		fveq1	$⊢ f = K \to f (0) = K (0)$
21	20	eqeq1d	$⊢ f = K \to (f (0) = P \leftrightarrow K (0) = P)$
22	19 21	anbi12d	$⊢ f = K \to ((F \circ f = G \land f (0) = P) \leftrightarrow (F \circ K = G \land K (0) = P))$
23	22	rspcev	$⊢ (K \in (II Cn C) \land (F \circ K = G \land K (0) = P)) \to \exists f \in (II Cn C) (F \circ f = G \land f (0) = P)$
24	15 16 17 23	syl12anc	$⊢ φ \to \exists f \in (II Cn C) (F \circ f = G \land f (0) = P)$
25		iiuni	$⊢ [0, 1] = ⋃ II$
26		iiconn	$⊢ II \in Conn$
27	26	a1i	$⊢ φ \to II \in Conn$
28		iinllyconn	$⊢ II \in N-LocallyConn$
29	28	a1i	$⊢ φ \to II \in N-LocallyConn$
30		0elunit	$⊢ 0 \in [0, 1]$
31	30	a1i	$⊢ φ \to 0 \in [0, 1]$
32	2 25 4 27 29 31 5 6 7	cvmliftmo	$⊢ φ \to \exists^{*} f \in (II Cn C) (F \circ f = G \land f (0) = P)$
33		reu5	$⊢ \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P) \leftrightarrow (\exists f \in (II Cn C) (F \circ f = G \land f (0) = P) \land \exists^{*} f \in (II Cn C) (F \circ f = G \land f (0) = P))$
34	24 32 33	sylanbrc	$⊢ φ \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P)$

Metamath Proof Explorer

Theorem cvmliftlem14

Proof