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	⊢ 𝐵 = ∪ 𝐶
	cvmliftmo.y	⊢ 𝑌 = ∪ 𝐾
	cvmliftmo.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
	cvmliftmo.k	⊢ ( 𝜑 → 𝐾 ∈ Conn )
	cvmliftmo.l	⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Conn )
	cvmliftmo.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
	cvmliftmoi.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐾 Cn 𝐶 ) )
	cvmliftmoi.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐾 Cn 𝐶 ) )
	cvmliftmoi.g	⊢ ( 𝜑 → ( 𝐹 ∘ 𝑀 ) = ( 𝐹 ∘ 𝑁 ) )
	cvmliftmoi.p	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑂 ) = ( 𝑁 ‘ 𝑂 ) )
Assertion	cvmliftmoi	⊢ ( 𝜑 → 𝑀 = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		cvmliftmo.b	⊢ 𝐵 = ∪ 𝐶
2		cvmliftmo.y	⊢ 𝑌 = ∪ 𝐾
3		cvmliftmo.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
4		cvmliftmo.k	⊢ ( 𝜑 → 𝐾 ∈ Conn )
5		cvmliftmo.l	⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Conn )
6		cvmliftmo.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
7		cvmliftmoi.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐾 Cn 𝐶 ) )
8		cvmliftmoi.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐾 Cn 𝐶 ) )
9		cvmliftmoi.g	⊢ ( 𝜑 → ( 𝐹 ∘ 𝑀 ) = ( 𝐹 ∘ 𝑁 ) )
10		cvmliftmoi.p	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑂 ) = ( 𝑁 ‘ 𝑂 ) )
11		eqid	⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
12	11	cvmscbv	⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑏 ∈ 𝐽 ↦ { 𝑚 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑚 = ( ◡ 𝐹 “ 𝑏 ) ∧ ∀ 𝑟 ∈ 𝑚 ( ∀ 𝑤 ∈ ( 𝑚 ∖ { 𝑟 } ) ( 𝑟 ∩ 𝑤 ) = ∅ ∧ ( 𝐹 ↾ 𝑟 ) ∈ ( ( 𝐶 ↾t 𝑟 ) Homeo ( 𝐽 ↾t 𝑏 ) ) ) ) } )
13	1 2 3 4 5 6 7 8 9 10 12	cvmliftmolem2	⊢ ( 𝜑 → 𝑀 = 𝑁 )