Metamath Proof Explorer

Theorem cvmliftlem5

Description: Lemma for cvmlift . Definition of Q at a successor. This is a function defined on W as ` ``' ( T |`I ) o. G where I is the unique covering set of 2nd( TM ) that contains Q ( M - 1 ) evaluated at the last defined point, namely ( M - 1 ) / N (note that for M = 1 this is using the seed value Q ( 0 ) ( 0 ) = P ). (Contributed by Mario Carneiro, 15-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 ⊢ S = k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
cvmliftlem.b ⊢ B = ⋃ C
cvmliftlem.x ⊢ X = ⋃ J
cvmliftlem.f ⊢ φ → F ∈ C CovMap J
cvmliftlem.g ⊢ φ → G ∈ II Cn J
cvmliftlem.p ⊢ φ → P ∈ B
cvmliftlem.e ⊢ φ → F ⁡ P = G ⁡ 0
cvmliftlem.n ⊢ φ → N ∈ ℕ
cvmliftlem.t ⊢ φ → T : 1 … N ⟶ ⋃ j ∈ J j × S ⁡ j
cvmliftlem.a ⊢ φ → ∀ k ∈ 1 … N G k − 1 N k N ⊆ 1 st ⁡ T ⁡ k
cvmliftlem.l ⊢ L = topGen ⁡ ran ⁡ .
cvmliftlem.q ⊢ Q = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P
cvmliftlem5.3 ⊢ W = M − 1 N M N
Assertion cvmliftlem5 ⊢ φ ∧ M ∈ ℕ → Q ⁡ M = z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 ⊢ S = k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
2 cvmliftlem.b ⊢ B = ⋃ C
3 cvmliftlem.x ⊢ X = ⋃ J
4 cvmliftlem.f ⊢ φ → F ∈ C CovMap J
5 cvmliftlem.g ⊢ φ → G ∈ II Cn J
6 cvmliftlem.p ⊢ φ → P ∈ B
7 cvmliftlem.e ⊢ φ → F ⁡ P = G ⁡ 0
8 cvmliftlem.n ⊢ φ → N ∈ ℕ
9 cvmliftlem.t ⊢ φ → T : 1 … N ⟶ ⋃ j ∈ J j × S ⁡ j
10 cvmliftlem.a ⊢ φ → ∀ k ∈ 1 … N G k − 1 N k N ⊆ 1 st ⁡ T ⁡ k
11 cvmliftlem.l ⊢ L = topGen ⁡ ran ⁡ .
12 cvmliftlem.q ⊢ Q = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P
13 cvmliftlem5.3 ⊢ W = M − 1 N M N
14 0z ⊢ 0 ∈ ℤ
15 simpr ⊢ φ ∧ M ∈ ℕ → M ∈ ℕ
16 nnuz ⊢ ℕ = ℤ ≥ 1
17 1e0p1 ⊢ 1 = 0 + 1
18 17 fveq2i ⊢ ℤ ≥ 1 = ℤ ≥ 0 + 1
19 16 18 eqtri ⊢ ℕ = ℤ ≥ 0 + 1
20 15 19 eleqtrdi ⊢ φ ∧ M ∈ ℕ → M ∈ ℤ ≥ 0 + 1
21 seqm1 ⊢ 0 ∈ ℤ ∧ M ∈ ℤ ≥ 0 + 1 → seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M − 1 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M
22 14 20 21 sylancr ⊢ φ ∧ M ∈ ℕ → seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M − 1 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M
23 12 fveq1i ⊢ Q ⁡ M = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M
24 12 fveq1i ⊢ Q ⁡ M − 1 = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M − 1
25 24 oveq1i ⊢ Q ⁡ M − 1 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M = seq 0 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M − 1 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M
26 22 23 25 3eqtr4g ⊢ φ ∧ M ∈ ℕ → Q ⁡ M = Q ⁡ M − 1 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M
27 0nnn ⊢ ¬ 0 ∈ ℕ
28 disjsn ⊢ ℕ ∩ 0 = ∅ ↔ ¬ 0 ∈ ℕ
29 27 28 mpbir ⊢ ℕ ∩ 0 = ∅
30 fnresi ⊢ I ↾ ℕ Fn ℕ
31 c0ex ⊢ 0 ∈ V
32 snex ⊢ 0 P ∈ V
33 31 32 fnsn ⊢ 0 0 P Fn 0
34 fvun1 ⊢ I ↾ ℕ Fn ℕ ∧ 0 0 P Fn 0 ∧ ℕ ∩ 0 = ∅ ∧ M ∈ ℕ → I ↾ ℕ ∪ 0 0 P ⁡ M = I ↾ ℕ ⁡ M
35 30 33 34 mp3an12 ⊢ ℕ ∩ 0 = ∅ ∧ M ∈ ℕ → I ↾ ℕ ∪ 0 0 P ⁡ M = I ↾ ℕ ⁡ M
36 29 15 35 sylancr ⊢ φ ∧ M ∈ ℕ → I ↾ ℕ ∪ 0 0 P ⁡ M = I ↾ ℕ ⁡ M
37 fvresi ⊢ M ∈ ℕ → I ↾ ℕ ⁡ M = M
38 37 adantl ⊢ φ ∧ M ∈ ℕ → I ↾ ℕ ⁡ M = M
39 36 38 eqtrd ⊢ φ ∧ M ∈ ℕ → I ↾ ℕ ∪ 0 0 P ⁡ M = M
40 39 oveq2d ⊢ φ ∧ M ∈ ℕ → Q ⁡ M − 1 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z I ↾ ℕ ∪ 0 0 P ⁡ M = Q ⁡ M − 1 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z M
41 fvexd ⊢ φ → Q ⁡ M − 1 ∈ V
42 simpr ⊢ x = Q ⁡ M − 1 ∧ m = M → m = M
43 42 oveq1d ⊢ x = Q ⁡ M − 1 ∧ m = M → m − 1 = M − 1
44 43 oveq1d ⊢ x = Q ⁡ M − 1 ∧ m = M → m − 1 N = M − 1 N
45 42 oveq1d ⊢ x = Q ⁡ M − 1 ∧ m = M → m N = M N
46 44 45 oveq12d ⊢ x = Q ⁡ M − 1 ∧ m = M → m − 1 N m N = M − 1 N M N
47 46 13 eqtr4di ⊢ x = Q ⁡ M − 1 ∧ m = M → m − 1 N m N = W
48 42 fveq2d ⊢ x = Q ⁡ M − 1 ∧ m = M → T ⁡ m = T ⁡ M
49 48 fveq2d ⊢ x = Q ⁡ M − 1 ∧ m = M → 2 nd ⁡ T ⁡ m = 2 nd ⁡ T ⁡ M
50 simpl ⊢ x = Q ⁡ M − 1 ∧ m = M → x = Q ⁡ M − 1
51 50 44 fveq12d ⊢ x = Q ⁡ M − 1 ∧ m = M → x ⁡ m − 1 N = Q ⁡ M − 1 ⁡ M − 1 N
52 51 eleq1d ⊢ x = Q ⁡ M − 1 ∧ m = M → x ⁡ m − 1 N ∈ b ↔ Q ⁡ M − 1 ⁡ M − 1 N ∈ b
53 49 52 riotaeqbidv ⊢ x = Q ⁡ M − 1 ∧ m = M → ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b = ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
54 53 reseq2d ⊢ x = Q ⁡ M − 1 ∧ m = M → F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b = F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b
55 54 cnveqd ⊢ x = Q ⁡ M − 1 ∧ m = M → F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 = F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1
56 55 fveq1d ⊢ x = Q ⁡ M − 1 ∧ m = M → F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z = F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
57 47 56 mpteq12dv ⊢ x = Q ⁡ M − 1 ∧ m = M → z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z = z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
58 eqid ⊢ x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z = x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z
59 ovex ⊢ M − 1 N M N ∈ V
60 13 59 eqeltri ⊢ W ∈ V
61 60 mptex ⊢ z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z ∈ V
62 57 58 61 ovmpoa ⊢ Q ⁡ M − 1 ∈ V ∧ M ∈ ℕ → Q ⁡ M − 1 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z M = z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
63 41 62 sylan ⊢ φ ∧ M ∈ ℕ → Q ⁡ M − 1 x ∈ V , m ∈ ℕ ⟼ z ∈ m − 1 N m N ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ m | x ⁡ m − 1 N ∈ b -1 ⁡ G ⁡ z M = z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z
64 26 40 63 3eqtrd ⊢ φ ∧ M ∈ ℕ → Q ⁡ M = z ∈ W ⟼ F ↾ ι b ∈ 2 nd ⁡ T ⁡ M | Q ⁡ M − 1 ⁡ M − 1 N ∈ b -1 ⁡ G ⁡ z