Theorem cvmliftlem1

Description: Lemma for cvmlift . In cvmliftlem15 , we picked an N large enough so that the sections ( G " [ ( k - 1 ) / N , k / N ] ) are all contained in an even covering, and the function T enumerates these even coverings. So 1st( TM ) is a neighborhood of ( G " [ ( M - 1 ) / N , M / N ] ) , and 2nd( TM ) is an even covering of 1st( TM ) , which is to say a disjoint union of open sets in C whose image is 1st( TM ) . (Contributed by Mario Carneiro, 14-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 (,) )
	cvmliftlem1.m	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
Assertion	cvmliftlem1	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) )

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		cvmliftlem1.m	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
13		relxp	⊢ Rel ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) )
14	13	rgenw	⊢ ∀ 𝑗 ∈ 𝐽 Rel ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) )
15		reliun	⊢ ( Rel ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐽 Rel ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
16	14 15	mpbir	⊢ Rel ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) )
17	9	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
18	17 12	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑇 ‘ 𝑀 ) ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
19		1st2nd	⊢ ( ( Rel ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ) → ( 𝑇 ‘ 𝑀 ) = ⟨ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) , ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ⟩ )
20	16 18 19	sylancr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑇 ‘ 𝑀 ) = ⟨ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) , ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ⟩ )
21	20 18	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) , ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ⟩ ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
22		fveq2	⊢ ( 𝑗 = ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) → ( 𝑆 ‘ 𝑗 ) = ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) )
23	22	opeliunxp2	⊢ ( ⟨ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) , ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ⟩ ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ↔ ( ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ 𝐽 ∧ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) )
24	23	simprbi	⊢ ( ⟨ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) , ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ⟩ ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) → ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) )
25	21 24	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) )