Metamath Proof Explorer

Theorem cvmlift

Description: One of the important properties of covering maps is that any path G in the base space "lifts" to a path f in the covering space such that F o. f = G , and given a starting point P in the covering space this lift is unique. The proof is contained in cvmliftlem1 thru cvmliftlem15 . (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypothesis cvmlift.1 ⊢B=⋃C
Assertion cvmlift ⊢F∈CCovMapJ∧G∈IICnJ∧P∈B∧F⁡P=G⁡0→∃!f∈IICnCF∘f=G∧f⁡0=P

Proof

Step Hyp Ref Expression
1 cvmlift.1 ⊢B=⋃C
2 eqid ⊢k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k=k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k
3 2 cvmscbv ⊢k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k=a∈J⟼b∈𝒫C∖∅|⋃b=F-1a∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡a
4 eqid ⊢⋃J=⋃J
5 simpll ⊢F∈CCovMapJ∧G∈IICnJ∧P∈B∧F⁡P=G⁡0→F∈CCovMapJ
6 simplr ⊢F∈CCovMapJ∧G∈IICnJ∧P∈B∧F⁡P=G⁡0→G∈IICnJ
7 simprl ⊢F∈CCovMapJ∧G∈IICnJ∧P∈B∧F⁡P=G⁡0→P∈B
8 simprr ⊢F∈CCovMapJ∧G∈IICnJ∧P∈B∧F⁡P=G⁡0→F⁡P=G⁡0
9 3 1 4 5 6 7 8 cvmliftlem15 ⊢F∈CCovMapJ∧G∈IICnJ∧P∈B∧F⁡P=G⁡0→∃!f∈IICnCF∘f=G∧f⁡0=P