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 ⊢ φ → F ∈ C CovMap J
cvmliftmo.k ⊢ φ → K ∈ Conn
cvmliftmo.l ⊢ φ → K ∈ N-Locally Conn
cvmliftmo.o ⊢ φ → O ∈ Y
cvmliftmoi.m ⊢ φ → M ∈ K Cn C
cvmliftmoi.n ⊢ φ → N ∈ K Cn C
cvmliftmoi.g ⊢ φ → F ∘ M = F ∘ N
cvmliftmoi.p ⊢ φ → M ⁡ O = N ⁡ O
Assertion cvmliftmoi ⊢ φ → M = N

Proof

Step Hyp Ref Expression
1 cvmliftmo.b ⊢ B = ⋃ C
2 cvmliftmo.y ⊢ Y = ⋃ K
3 cvmliftmo.f ⊢ φ → F ∈ C CovMap J
4 cvmliftmo.k ⊢ φ → K ∈ Conn
5 cvmliftmo.l ⊢ φ → K ∈ N-Locally Conn
6 cvmliftmo.o ⊢ φ → O ∈ Y
7 cvmliftmoi.m ⊢ φ → M ∈ K Cn C
8 cvmliftmoi.n ⊢ φ → N ∈ K Cn C
9 cvmliftmoi.g ⊢ φ → F ∘ M = F ∘ N
10 cvmliftmoi.p ⊢ φ → M ⁡ O = N ⁡ O
11 eqid ⊢ k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k = k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
12 11 cvmscbv ⊢ k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k = b ∈ J ⟼ m ∈ 𝒫 C ∖ ∅ | ⋃ m = F -1 b ∧ ∀ r ∈ m ∀ w ∈ m ∖ r r ∩ w = ∅ ∧ F ↾ r ∈ C ↾ 𝑡 r Homeo J ↾ 𝑡 b
13 1 2 3 4 5 6 7 8 9 10 12 cvmliftmolem2 ⊢ φ → M = N