Theorem cvmliftlem14

Description: Lemma for cvmlift . Putting the results of cvmliftlem11 , cvmliftlem13 and cvmliftmo together, we have that K is a continuous function, satisfies F o. K = G and K ( 0 ) = P , and is equal to any other function which also has these properties, so it follows that K is the unique lift of G . (Contributed by Mario Carneiro, 16-Feb-2015)

	Ref	Expression
Hypotheses	cvmliftlem.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
	cvmliftlem.b	⊢ 𝐵 = ∪ 𝐶
	cvmliftlem.x	⊢ 𝑋 = ∪ 𝐽
	cvmliftlem.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
	cvmliftlem.g	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
	cvmliftlem.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	cvmliftlem.e	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
	cvmliftlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	cvmliftlem.t	⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
	cvmliftlem.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
	cvmliftlem.l	⊢ 𝐿 = ( topGen ‘ ran (,) )
	cvmliftlem.q	⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
	cvmliftlem.k	⊢ 𝐾 = ∪ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑘 )
Assertion	cvmliftlem14	⊢ ( 𝜑 → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		cvmliftlem.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2		cvmliftlem.b	⊢ 𝐵 = ∪ 𝐶
3		cvmliftlem.x	⊢ 𝑋 = ∪ 𝐽
4		cvmliftlem.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
5		cvmliftlem.g	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
6		cvmliftlem.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
7		cvmliftlem.e	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
8		cvmliftlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9		cvmliftlem.t	⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
10		cvmliftlem.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
11		cvmliftlem.l	⊢ 𝐿 = ( topGen ‘ ran (,) )
12		cvmliftlem.q	⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
13		cvmliftlem.k	⊢ 𝐾 = ∪ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑘 )
14	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem11	⊢ ( 𝜑 → ( 𝐾 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = 𝐺 ) )
15	14	simpld	⊢ ( 𝜑 → 𝐾 ∈ ( II Cn 𝐶 ) )
16	14	simprd	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐾 ) = 𝐺 )
17	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem13	⊢ ( 𝜑 → ( 𝐾 ‘ 0 ) = 𝑃 )
18		coeq2	⊢ ( 𝑓 = 𝐾 → ( 𝐹 ∘ 𝑓 ) = ( 𝐹 ∘ 𝐾 ) )
19	18	eqeq1d	⊢ ( 𝑓 = 𝐾 → ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ↔ ( 𝐹 ∘ 𝐾 ) = 𝐺 ) )
20		fveq1	⊢ ( 𝑓 = 𝐾 → ( 𝑓 ‘ 0 ) = ( 𝐾 ‘ 0 ) )
21	20	eqeq1d	⊢ ( 𝑓 = 𝐾 → ( ( 𝑓 ‘ 0 ) = 𝑃 ↔ ( 𝐾 ‘ 0 ) = 𝑃 ) )
22	19 21	anbi12d	⊢ ( 𝑓 = 𝐾 → ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝐾 ) = 𝐺 ∧ ( 𝐾 ‘ 0 ) = 𝑃 ) ) )
23	22	rspcev	⊢ ( ( 𝐾 ∈ ( II Cn 𝐶 ) ∧ ( ( 𝐹 ∘ 𝐾 ) = 𝐺 ∧ ( 𝐾 ‘ 0 ) = 𝑃 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
24	15 16 17 23	syl12anc	⊢ ( 𝜑 → ∃ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
25		iiuni	⊢ ( 0 [,] 1 ) = ∪ II
26		iiconn	⊢ II ∈ Conn
27	26	a1i	⊢ ( 𝜑 → II ∈ Conn )
28		iinllyconn	⊢ II ∈ 𝑛-Locally Conn
29	28	a1i	⊢ ( 𝜑 → II ∈ 𝑛-Locally Conn )
30		0elunit	⊢ 0 ∈ ( 0 [,] 1 )
31	30	a1i	⊢ ( 𝜑 → 0 ∈ ( 0 [,] 1 ) )
32	2 25 4 27 29 31 5 6 7	cvmliftmo	⊢ ( 𝜑 → ∃* 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
33		reu5	⊢ ( ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ↔ ( ∃ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ∧ ∃* 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) )
34	24 32 33	sylanbrc	⊢ ( 𝜑 → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )