cvmliftmo

Description: A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015) (Revised by NM, 17-Jun-2017)

	Ref	Expression
Hypotheses	cvmliftmo.b	$⊢ B = ⋃ C$
	cvmliftmo.y	$⊢ Y = ⋃ K$
	cvmliftmo.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftmo.k	$⊢ φ \to K \in Conn$
	cvmliftmo.l	$⊢ φ \to K \in N-LocallyConn$
	cvmliftmo.o	$⊢ φ \to O \in Y$
	cvmliftmo.g	$⊢ φ \to G \in (K Cn J)$
	cvmliftmo.p	$⊢ φ \to P \in B$
	cvmliftmo.e	$⊢ φ \to F (P) = G (O)$
Assertion	cvmliftmo	$⊢ φ \to \exists^{*} f \in (K Cn C) (F \circ f = G \land f (O) = P)$

Proof

Step	Hyp	Ref	Expression
1		cvmliftmo.b	$⊢ B = ⋃ C$
2		cvmliftmo.y	$⊢ Y = ⋃ K$
3		cvmliftmo.f	$⊢ φ \to F \in (C CovMap J)$
4		cvmliftmo.k	$⊢ φ \to K \in Conn$
5		cvmliftmo.l	$⊢ φ \to K \in N-LocallyConn$
6		cvmliftmo.o	$⊢ φ \to O \in Y$
7		cvmliftmo.g	$⊢ φ \to G \in (K Cn J)$
8		cvmliftmo.p	$⊢ φ \to P \in B$
9		cvmliftmo.e	$⊢ φ \to F (P) = G (O)$
10	3	ad2antrr	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to F \in (C CovMap J)$
11	4	ad2antrr	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to K \in Conn$
12	5	ad2antrr	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to K \in N-LocallyConn$
13	6	ad2antrr	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to O \in Y$
14		simplrl	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to f \in (K Cn C)$
15		simplrr	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to g \in (K Cn C)$
16		simprll	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to F \circ f = G$
17		simprrl	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to F \circ g = G$
18	16 17	eqtr4d	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to F \circ f = F \circ g$
19		simprlr	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to f (O) = P$
20		simprrr	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to g (O) = P$
21	19 20	eqtr4d	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to f (O) = g (O)$
22	1 2 10 11 12 13 14 15 18 21	cvmliftmoi	$⊢ ((φ \land (f \in (K Cn C) \land g \in (K Cn C))) \land ((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P))) \to f = g$
23	22	ex	$⊢ (φ \land (f \in (K Cn C) \land g \in (K Cn C))) \to (((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P)) \to f = g)$
24	23	ralrimivva	$⊢ φ \to \forall f \in (K Cn C) \forall g \in (K Cn C) (((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P)) \to f = g)$
25		coeq2	$⊢ f = g \to F \circ f = F \circ g$
26	25	eqeq1d	$⊢ f = g \to (F \circ f = G \leftrightarrow F \circ g = G)$
27		fveq1	$⊢ f = g \to f (O) = g (O)$
28	27	eqeq1d	$⊢ f = g \to (f (O) = P \leftrightarrow g (O) = P)$
29	26 28	anbi12d	$⊢ f = g \to ((F \circ f = G \land f (O) = P) \leftrightarrow (F \circ g = G \land g (O) = P))$
30	29	rmo4	$⊢ \exists^{*} f \in (K Cn C) (F \circ f = G \land f (O) = P) \leftrightarrow \forall f \in (K Cn C) \forall g \in (K Cn C) (((F \circ f = G \land f (O) = P) \land (F \circ g = G \land g (O) = P)) \to f = g)$
31	24 30	sylibr	$⊢ φ \to \exists^{*} f \in (K Cn C) (F \circ f = G \land f (O) = P)$

Metamath Proof Explorer

Theorem cvmliftmo

Proof