Metamath Proof Explorer

Theorem cvmliftlem13

Description: Lemma for cvmlift . The initial value of K is P because Q ( 1 ) is a subset of K which takes value P at 0 . (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 cvmliftlem13 ( 𝜑 → ( 𝐾 ‘ 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 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
17 16 2 cnf ⊢ ( 𝐾 ∈ ( II Cn 𝐶 ) → 𝐾 : ( 0 [,] 1 ) ⟶ 𝐵 )
18 15 17 syl ⊢ ( 𝜑 → 𝐾 : ( 0 [,] 1 ) ⟶ 𝐵 )
19 18 ffund ⊢ ( 𝜑 → Fun 𝐾 )
20 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
21 8 20 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
22 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑁 ) )
23 21 22 syl ⊢ ( 𝜑 → 1 ∈ ( 1 ... 𝑁 ) )
24 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 1 ) )
25 24 ssiun2s ⊢ ( 1 ∈ ( 1 ... 𝑁 ) → ( 𝑄 ‘ 1 ) ⊆ ∪ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑘 ) )
26 23 25 syl ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ⊆ ∪ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑘 ) )
27 26 13 sseqtrrdi ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ⊆ 𝐾 )
28 0xr ⊢ 0 ∈ ℝ*
29 28 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
30 8 nnrecred ⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ )
31 30 rexrd ⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ* )
32 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
33 0le1 ⊢ 0 ≤ 1
34 33 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
35 8 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
36 8 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
37 divge0 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → 0 ≤ ( 1 / 𝑁 ) )
38 32 34 35 36 37 syl22anc ⊢ ( 𝜑 → 0 ≤ ( 1 / 𝑁 ) )
39 lbicc2 ⊢ ( ( 0 ∈ ℝ* ∧ ( 1 / 𝑁 ) ∈ ℝ* ∧ 0 ≤ ( 1 / 𝑁 ) ) → 0 ∈ ( 0 [,] ( 1 / 𝑁 ) ) )
40 29 31 38 39 syl3anc ⊢ ( 𝜑 → 0 ∈ ( 0 [,] ( 1 / 𝑁 ) ) )
41 1m1e0 ⊢ ( 1 − 1 ) = 0
42 41 oveq1i ⊢ ( ( 1 − 1 ) / 𝑁 ) = ( 0 / 𝑁 )
43 8 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
44 8 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
45 43 44 div0d ⊢ ( 𝜑 → ( 0 / 𝑁 ) = 0 )
46 42 45 eqtrid ⊢ ( 𝜑 → ( ( 1 − 1 ) / 𝑁 ) = 0 )
47 46 oveq1d ⊢ ( 𝜑 → ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) = ( 0 [,] ( 1 / 𝑁 ) ) )
48 40 47 eleqtrrd ⊢ ( 𝜑 → 0 ∈ ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) )
49 eqid ⊢ ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) = ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) )
50 simpr ⊢ ( ( 𝜑 ∧ 1 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ( 1 ... 𝑁 ) )
51 1 2 3 4 5 6 7 8 9 10 11 12 49 cvmliftlem7 ⊢ ( ( 𝜑 ∧ 1 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 1 − 1 ) ) ‘ ( ( 1 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 1 − 1 ) / 𝑁 ) ) } ) )
52 1 2 3 4 5 6 7 8 9 10 11 12 49 50 51 cvmliftlem6 ⊢ ( ( 𝜑 ∧ 1 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ 1 ) : ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) ) )
53 23 52 mpdan ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) : ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) ) )
54 53 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) : ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ⟶ 𝐵 )
55 54 fdmd ⊢ ( 𝜑 → dom ( 𝑄 ‘ 1 ) = ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) )
56 48 55 eleqtrrd ⊢ ( 𝜑 → 0 ∈ dom ( 𝑄 ‘ 1 ) )
57 funssfv ⊢ ( ( Fun 𝐾 ∧ ( 𝑄 ‘ 1 ) ⊆ 𝐾 ∧ 0 ∈ dom ( 𝑄 ‘ 1 ) ) → ( 𝐾 ‘ 0 ) = ( ( 𝑄 ‘ 1 ) ‘ 0 ) )
58 19 27 56 57 syl3anc ⊢ ( 𝜑 → ( 𝐾 ‘ 0 ) = ( ( 𝑄 ‘ 1 ) ‘ 0 ) )
59 1 2 3 4 5 6 7 8 9 10 11 12 cvmliftlem9 ⊢ ( ( 𝜑 ∧ 1 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ 1 ) ‘ ( ( 1 − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ ( 1 − 1 ) ) ‘ ( ( 1 − 1 ) / 𝑁 ) ) )
60 23 59 mpdan ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) ‘ ( ( 1 − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ ( 1 − 1 ) ) ‘ ( ( 1 − 1 ) / 𝑁 ) ) )
61 46 fveq2d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) ‘ ( ( 1 − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ 1 ) ‘ 0 ) )
62 41 fveq2i ⊢ ( 𝑄 ‘ ( 1 − 1 ) ) = ( 𝑄 ‘ 0 )
63 1 2 3 4 5 6 7 8 9 10 11 12 cvmliftlem4 ⊢ ( 𝑄 ‘ 0 ) = { ⟨ 0 , 𝑃 ⟩ }
64 62 63 eqtri ⊢ ( 𝑄 ‘ ( 1 − 1 ) ) = { ⟨ 0 , 𝑃 ⟩ }
65 64 a1i ⊢ ( 𝜑 → ( 𝑄 ‘ ( 1 − 1 ) ) = { ⟨ 0 , 𝑃 ⟩ } )
66 65 46 fveq12d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 1 − 1 ) ) ‘ ( ( 1 − 1 ) / 𝑁 ) ) = ( { ⟨ 0 , 𝑃 ⟩ } ‘ 0 ) )
67 60 61 66 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) ‘ 0 ) = ( { ⟨ 0 , 𝑃 ⟩ } ‘ 0 ) )
68 0nn0 ⊢ 0 ∈ ℕ0
69 fvsng ⊢ ( ( 0 ∈ ℕ0 ∧ 𝑃 ∈ 𝐵 ) → ( { ⟨ 0 , 𝑃 ⟩ } ‘ 0 ) = 𝑃 )
70 68 6 69 sylancr ⊢ ( 𝜑 → ( { ⟨ 0 , 𝑃 ⟩ } ‘ 0 ) = 𝑃 )
71 58 67 70 3eqtrd ⊢ ( 𝜑 → ( 𝐾 ‘ 0 ) = 𝑃 )