Metamath Proof Explorer

Theorem cvmlift3

Description: A general version of cvmlift . If K is simply connected and weakly locally path-connected, then there is a unique lift of functions on K which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015)

Ref Expression
Hypotheses cvmlift3.b ⊢ 𝐵 = ∪ 𝐶
cvmlift3.y ⊢ 𝑌 = ∪ 𝐾
cvmlift3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmlift3.k ⊢ ( 𝜑 → 𝐾 ∈ SConn )
cvmlift3.l ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally PConn )
cvmlift3.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
cvmlift3.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
cvmlift3.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmlift3.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
Assertion cvmlift3 ( 𝜑 → ∃! 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 cvmlift3.b ⊢ 𝐵 = ∪ 𝐶
2 cvmlift3.y ⊢ 𝑌 = ∪ 𝐾
3 cvmlift3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
4 cvmlift3.k ⊢ ( 𝜑 → 𝐾 ∈ SConn )
5 cvmlift3.l ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally PConn )
6 cvmlift3.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
7 cvmlift3.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
8 cvmlift3.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
9 cvmlift3.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
10 eqeq2 ⊢ ( 𝑏 = 𝑧 → ( ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑏 ↔ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )
11 10 3anbi3d ⊢ ( 𝑏 = 𝑧 → ( ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑏 ) ↔ ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
12 11 rexbidv ⊢ ( 𝑏 = 𝑧 → ( ∃ 𝑐 ∈ ( II Cn 𝐾 ) ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑏 ) ↔ ∃ 𝑐 ∈ ( II Cn 𝐾 ) ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
13 12 cbvriotavw ⊢ ( ℩ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ ( II Cn 𝐾 ) ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑏 ) ) = ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑐 ∈ ( II Cn 𝐾 ) ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )
14 fveq1 ⊢ ( 𝑐 = 𝑓 → ( 𝑐 ‘ 0 ) = ( 𝑓 ‘ 0 ) )
15 14 eqeq1d ⊢ ( 𝑐 = 𝑓 → ( ( 𝑐 ‘ 0 ) = 𝑂 ↔ ( 𝑓 ‘ 0 ) = 𝑂 ) )
16 fveq1 ⊢ ( 𝑐 = 𝑓 → ( 𝑐 ‘ 1 ) = ( 𝑓 ‘ 1 ) )
17 16 eqeq1d ⊢ ( 𝑐 = 𝑓 → ( ( 𝑐 ‘ 1 ) = 𝑎 ↔ ( 𝑓 ‘ 1 ) = 𝑎 ) )
18 coeq2 ⊢ ( 𝑑 = 𝑔 → ( 𝐹 ∘ 𝑑 ) = ( 𝐹 ∘ 𝑔 ) )
19 18 eqeq1d ⊢ ( 𝑑 = 𝑔 → ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑐 ) ) )
20 fveq1 ⊢ ( 𝑑 = 𝑔 → ( 𝑑 ‘ 0 ) = ( 𝑔 ‘ 0 ) )
21 20 eqeq1d ⊢ ( 𝑑 = 𝑔 → ( ( 𝑑 ‘ 0 ) = 𝑃 ↔ ( 𝑔 ‘ 0 ) = 𝑃 ) )
22 19 21 anbi12d ⊢ ( 𝑑 = 𝑔 → ( ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
23 22 cbvriotavw ⊢ ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
24 coeq2 ⊢ ( 𝑐 = 𝑓 → ( 𝐺 ∘ 𝑐 ) = ( 𝐺 ∘ 𝑓 ) )
25 24 eqeq2d ⊢ ( 𝑐 = 𝑓 → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑐 ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ) )
26 25 anbi1d ⊢ ( 𝑐 = 𝑓 → ( ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
27 26 riotabidv ⊢ ( 𝑐 = 𝑓 → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
28 23 27 syl5eq ⊢ ( 𝑐 = 𝑓 → ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
29 28 fveq1d ⊢ ( 𝑐 = 𝑓 → ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )
30 29 eqeq1d ⊢ ( 𝑐 = 𝑓 → ( ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ↔ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )
31 15 17 30 3anbi123d ⊢ ( 𝑐 = 𝑓 → ( ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
32 31 cbvrexvw ⊢ ( ∃ 𝑐 ∈ ( II Cn 𝐾 ) ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )
33 eqeq2 ⊢ ( 𝑎 = 𝑥 → ( ( 𝑓 ‘ 1 ) = 𝑎 ↔ ( 𝑓 ‘ 1 ) = 𝑥 ) )
34 33 3anbi2d ⊢ ( 𝑎 = 𝑥 → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
35 34 rexbidv ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
36 32 35 syl5bb ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑐 ∈ ( II Cn 𝐾 ) ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
37 36 riotabidv ⊢ ( 𝑎 = 𝑥 → ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑐 ∈ ( II Cn 𝐾 ) ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) = ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
38 13 37 syl5eq ⊢ ( 𝑎 = 𝑥 → ( ℩ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ ( II Cn 𝐾 ) ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑏 ) ) = ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
39 38 cbvmptv ⊢ ( 𝑎 ∈ 𝑌 ↦ ( ℩ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ ( II Cn 𝐾 ) ( ( 𝑐 ‘ 0 ) = 𝑂 ∧ ( 𝑐 ‘ 1 ) = 𝑎 ∧ ( ( ℩ 𝑑 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑑 ) = ( 𝐺 ∘ 𝑐 ) ∧ ( 𝑑 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑏 ) ) ) = ( 𝑥 ∈ 𝑌 ↦ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
40 eqid ⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
41 40 cvmscbv ⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑎 ∈ 𝐽 ↦ { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑣 ∈ 𝑏 ( ∀ 𝑢 ∈ ( 𝑏 ∖ { 𝑣 } ) ( 𝑣 ∩ 𝑢 ) = ∅ ∧ ( 𝐹 ↾ 𝑣 ) ∈ ( ( 𝐶 ↾t 𝑣 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) } )
42 1 2 3 4 5 6 7 8 9 39 41 cvmlift3lem9 ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) )
43 sconnpconn ⊢ ( 𝐾 ∈ SConn → 𝐾 ∈ PConn )
44 pconnconn ⊢ ( 𝐾 ∈ PConn → 𝐾 ∈ Conn )
45 4 43 44 3syl ⊢ ( 𝜑 → 𝐾 ∈ Conn )
46 pconnconn ⊢ ( 𝑥 ∈ PConn → 𝑥 ∈ Conn )
47 46 ssriv ⊢ PConn ⊆ Conn
48 nllyss ⊢ ( PConn ⊆ Conn → 𝑛-Locally PConn ⊆ 𝑛-Locally Conn )
49 47 48 ax-mp ⊢ 𝑛-Locally PConn ⊆ 𝑛-Locally Conn
50 49 5 sselid ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Conn )
51 1 2 3 45 50 6 7 8 9 cvmliftmo ⊢ ( 𝜑 → ∃* 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) )
52 reu5 ⊢ ( ∃! 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ↔ ( ∃ 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ∃* 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ) )
53 42 51 52 sylanbrc ⊢ ( 𝜑 → ∃! 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) )