cvmlift3

Description: A general version of cvmlift . If K is simply connected and weakly locally path-connected, then there is a unique lift of functions on K which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015)

	Ref	Expression
Hypotheses	cvmlift3.b	$⊢ B = ⋃ C$
	cvmlift3.y	$⊢ Y = ⋃ K$
	cvmlift3.f	$⊢ φ \to F \in (C CovMap J)$
	cvmlift3.k	$⊢ φ \to K \in SConn$
	cvmlift3.l	$⊢ φ \to K \in N-LocallyPConn$
	cvmlift3.o	$⊢ φ \to O \in Y$
	cvmlift3.g	$⊢ φ \to G \in (K Cn J)$
	cvmlift3.p	$⊢ φ \to P \in B$
	cvmlift3.e	$⊢ φ \to F (P) = G (O)$
Assertion	cvmlift3	$⊢ φ \to \exists! f \in (K Cn C) (F \circ f = G \land f (O) = P)$

Proof

Step	Hyp	Ref	Expression
1		cvmlift3.b	$⊢ B = ⋃ C$
2		cvmlift3.y	$⊢ Y = ⋃ K$
3		cvmlift3.f	$⊢ φ \to F \in (C CovMap J)$
4		cvmlift3.k	$⊢ φ \to K \in SConn$
5		cvmlift3.l	$⊢ φ \to K \in N-LocallyPConn$
6		cvmlift3.o	$⊢ φ \to O \in Y$
7		cvmlift3.g	$⊢ φ \to G \in (K Cn J)$
8		cvmlift3.p	$⊢ φ \to P \in B$
9		cvmlift3.e	$⊢ φ \to F (P) = G (O)$
10		eqeq2	$⊢ b = z \to ((ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = b \leftrightarrow (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = z)$
11	10	3anbi3d	$⊢ b = z \to ((c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = b) \leftrightarrow (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = z))$
12	11	rexbidv	$⊢ b = z \to (\exists c \in (II Cn K) (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = b) \leftrightarrow \exists c \in (II Cn K) (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = z))$
13	12	cbvriotavw	$⊢ (ι b \in B \| \exists c \in (II Cn K) (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = b)) = (ι z \in B \| \exists c \in (II Cn K) (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = z))$
14		fveq1	$⊢ c = f \to c (0) = f (0)$
15	14	eqeq1d	$⊢ c = f \to (c (0) = O \leftrightarrow f (0) = O)$
16		fveq1	$⊢ c = f \to c (1) = f (1)$
17	16	eqeq1d	$⊢ c = f \to (c (1) = a \leftrightarrow f (1) = a)$
18		coeq2	$⊢ d = g \to F \circ d = F \circ g$
19	18	eqeq1d	$⊢ d = g \to (F \circ d = G \circ c \leftrightarrow F \circ g = G \circ c)$
20		fveq1	$⊢ d = g \to d (0) = g (0)$
21	20	eqeq1d	$⊢ d = g \to (d (0) = P \leftrightarrow g (0) = P)$
22	19 21	anbi12d	$⊢ d = g \to ((F \circ d = G \circ c \land d (0) = P) \leftrightarrow (F \circ g = G \circ c \land g (0) = P))$
23	22	cbvriotavw	$⊢ (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \circ c \land g (0) = P))$
24		coeq2	$⊢ c = f \to G \circ c = G \circ f$
25	24	eqeq2d	$⊢ c = f \to (F \circ g = G \circ c \leftrightarrow F \circ g = G \circ f)$
26	25	anbi1d	$⊢ c = f \to ((F \circ g = G \circ c \land g (0) = P) \leftrightarrow (F \circ g = G \circ f \land g (0) = P))$
27	26	riotabidv	$⊢ c = f \to (ι g \in (II Cn C) \| (F \circ g = G \circ c \land g (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P))$
28	23 27	syl5eq	$⊢ c = f \to (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P))$
29	28	fveq1d	$⊢ c = f \to (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1)$
30	29	eqeq1d	$⊢ c = f \to ((ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = z \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z)$
31	15 17 30	3anbi123d	$⊢ c = f \to ((c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = z) \leftrightarrow (f (0) = O \land f (1) = a \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z))$
32	31	cbvrexvw	$⊢ \exists c \in (II Cn K) (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = z) \leftrightarrow \exists f \in (II Cn K) (f (0) = O \land f (1) = a \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z)$
33		eqeq2	$⊢ a = x \to (f (1) = a \leftrightarrow f (1) = x)$
34	33	3anbi2d	$⊢ a = x \to ((f (0) = O \land f (1) = a \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z) \leftrightarrow (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z))$
35	34	rexbidv	$⊢ a = x \to (\exists f \in (II Cn K) (f (0) = O \land f (1) = a \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z) \leftrightarrow \exists f \in (II Cn K) (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z))$
36	32 35	syl5bb	$⊢ a = x \to (\exists c \in (II Cn K) (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = z) \leftrightarrow \exists f \in (II Cn K) (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z))$
37	36	riotabidv	$⊢ a = x \to (ι z \in B \| \exists c \in (II Cn K) (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = z)) = (ι z \in B \| \exists f \in (II Cn K) (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z))$
38	13 37	syl5eq	$⊢ a = x \to (ι b \in B \| \exists c \in (II Cn K) (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = b)) = (ι z \in B \| \exists f \in (II Cn K) (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z))$
39	38	cbvmptv	$⊢ (a \in Y ⟼ (ι b \in B \| \exists c \in (II Cn K) (c (0) = O \land c (1) = a \land (ι d \in (II Cn C) \| (F \circ d = G \circ c \land d (0) = P)) (1) = b))) = (x \in Y ⟼ (ι z \in B \| \exists f \in (II Cn K) (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z)))$
40		eqid	$⊢ (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall c \in s (\forall d \in (s ∖ \{c\}) c \cap d = \emptyset \land {F ↾}_{c} \in ((C ↾_{𝑡} c) Homeo (J ↾_{𝑡} k))))\}) = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall c \in s (\forall d \in (s ∖ \{c\}) c \cap d = \emptyset \land {F ↾}_{c} \in ((C ↾_{𝑡} c) Homeo (J ↾_{𝑡} k))))\})$
41	40	cvmscbv	$⊢ (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall c \in s (\forall d \in (s ∖ \{c\}) c \cap d = \emptyset \land {F ↾}_{c} \in ((C ↾_{𝑡} c) Homeo (J ↾_{𝑡} k))))\}) = (a \in J ⟼ \{b \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ b = F^{-1} [a] \land \forall v \in b (\forall u \in (b ∖ \{v\}) v \cap u = \emptyset \land {F ↾}_{v} \in ((C ↾_{𝑡} v) Homeo (J ↾_{𝑡} a))))\})$
42	1 2 3 4 5 6 7 8 9 39 41	cvmlift3lem9	$⊢ φ \to \exists f \in (K Cn C) (F \circ f = G \land f (O) = P)$
43		sconnpconn	$⊢ K \in SConn \to K \in PConn$
44		pconnconn	$⊢ K \in PConn \to K \in Conn$
45	4 43 44	3syl	$⊢ φ \to K \in Conn$
46		pconnconn	$⊢ x \in PConn \to x \in Conn$
47	46	ssriv	$⊢ PConn \subseteq Conn$
48		nllyss	$⊢ PConn \subseteq Conn \to N-LocallyPConn\subseteqN-LocallyConn$
49	47 48	ax-mp	$⊢ N-LocallyPConn\subseteqN-LocallyConn$
50	49 5	sseldi	$⊢ φ \to K \in N-LocallyConn$
51	1 2 3 45 50 6 7 8 9	cvmliftmo	$⊢ φ \to \exists^{*} f \in (K Cn C) (F \circ f = G \land f (O) = P)$
52		reu5	$⊢ \exists! f \in (K Cn C) (F \circ f = G \land f (O) = P) \leftrightarrow (\exists f \in (K Cn C) (F \circ f = G \land f (O) = P) \land \exists^{*} f \in (K Cn C) (F \circ f = G \land f (O) = P))$
53	42 51 52	sylanbrc	$⊢ φ \to \exists! f \in (K Cn C) (F \circ f = G \land f (O) = P)$

Metamath Proof Explorer

Theorem cvmlift3

Proof