Metamath Proof Explorer

Theorem cvmliftmoi

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)

		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$
		cvmliftmoi.m	$⊢ φ \to M \in (K Cn C)$
		cvmliftmoi.n	$⊢ φ \to N \in (K Cn C)$
		cvmliftmoi.g	$⊢ φ \to F \circ M = F \circ N$
		cvmliftmoi.p	$⊢ φ \to M (O) = N (O)$
	Assertion	cvmliftmoi	$⊢ φ \to M = N$

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		cvmliftmoi.m	$⊢ φ \to M \in (K Cn C)$
8		cvmliftmoi.n	$⊢ φ \to N \in (K Cn C)$
9		cvmliftmoi.g	$⊢ φ \to F \circ M = F \circ N$
10		cvmliftmoi.p	$⊢ φ \to M (O) = N (O)$
11		eqid	$⊢ (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))))\}) = (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))))\})$
12	11	cvmscbv	$⊢ (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))))\}) = (b \in J ⟼ \{m \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ m = F^{-1} [b] \land \forall r \in m (\forall w \in (m ∖ \{r\}) r \cap w = \emptyset \land {F ↾}_{r} \in ((C ↾_{𝑡} r) Homeo (J ↾_{𝑡} b))))\})$
13	1 2 3 4 5 6 7 8 9 10 12	cvmliftmolem2	$⊢ φ \to M = N$