Theorem cvmliftlem2

Description: Lemma for cvmlift . W = [ ( k - 1 ) / N , k / N ] is a subset of [ 0 , 1 ] for each M e. ( 1 ... N ) . (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 (,) )
	cvmliftlem1.m	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
	cvmliftlem3.3	⊢ 𝑊 = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) )
Assertion	cvmliftlem2	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ⊆ ( 0 [,] 1 ) )

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		cvmliftlem3.3	⊢ 𝑊 = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) )
14		0red	⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ∈ ℝ )
15		1red	⊢ ( ( 𝜑 ∧ 𝜓 ) → 1 ∈ ℝ )
16		elfznn	⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → 𝑀 ∈ ℕ )
17	12 16	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ℕ )
18	17	nnred	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ℝ )
19		peano2rem	⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 1 ) ∈ ℝ )
20	18 19	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 − 1 ) ∈ ℝ )
21		nnm1nn0	⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ0 )
22	17 21	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 − 1 ) ∈ ℕ0 )
23	22	nn0ge0d	⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ≤ ( 𝑀 − 1 ) )
24	8	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ ℕ )
25	24	nnred	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ ℝ )
26	24	nngt0d	⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 < 𝑁 )
27		divge0	⊢ ( ( ( ( 𝑀 − 1 ) ∈ ℝ ∧ 0 ≤ ( 𝑀 − 1 ) ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → 0 ≤ ( ( 𝑀 − 1 ) / 𝑁 ) )
28	20 23 25 26 27	syl22anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ≤ ( ( 𝑀 − 1 ) / 𝑁 ) )
29		elfzle2	⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → 𝑀 ≤ 𝑁 )
30	12 29	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ≤ 𝑁 )
31	24	nncnd	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ ℂ )
32	31	mulid1d	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑁 · 1 ) = 𝑁 )
33	30 32	breqtrrd	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ≤ ( 𝑁 · 1 ) )
34		ledivmul	⊢ ( ( 𝑀 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑀 / 𝑁 ) ≤ 1 ↔ 𝑀 ≤ ( 𝑁 · 1 ) ) )
35	18 15 25 26 34	syl112anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑀 / 𝑁 ) ≤ 1 ↔ 𝑀 ≤ ( 𝑁 · 1 ) ) )
36	33 35	mpbird	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 / 𝑁 ) ≤ 1 )
37		iccss	⊢ ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ ( ( 𝑀 − 1 ) / 𝑁 ) ∧ ( 𝑀 / 𝑁 ) ≤ 1 ) ) → ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) ⊆ ( 0 [,] 1 ) )
38	14 15 28 36 37	syl22anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) ⊆ ( 0 [,] 1 ) )
39	13 38	eqsstrid	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ⊆ ( 0 [,] 1 ) )