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 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
cvmliftlem.k K = k = 1 N Q k
Assertion cvmliftlem13 φ K 0 = P

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 cvmliftlem.k K = k = 1 N Q k
14 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem11 φ K II Cn C F K = G
15 14 simpld φ K II Cn C
16 iiuni 0 1 = II
17 16 2 cnf K II Cn C K : 0 1 B
18 15 17 syl φ K : 0 1 B
19 18 ffund φ Fun K
20 nnuz = 1
21 8 20 eleqtrdi φ N 1
22 eluzfz1 N 1 1 1 N
23 21 22 syl φ 1 1 N
24 fveq2 k = 1 Q k = Q 1
25 24 ssiun2s 1 1 N Q 1 k = 1 N Q k
26 23 25 syl φ Q 1 k = 1 N Q k
27 26 13 sseqtrrdi φ Q 1 K
28 0xr 0 *
29 28 a1i φ 0 *
30 8 nnrecred φ 1 N
31 30 rexrd φ 1 N *
32 1red φ 1
33 0le1 0 1
34 33 a1i φ 0 1
35 8 nnred φ N
36 8 nngt0d φ 0 < N
37 divge0 1 0 1 N 0 < N 0 1 N
38 32 34 35 36 37 syl22anc φ 0 1 N
39 lbicc2 0 * 1 N * 0 1 N 0 0 1 N
40 29 31 38 39 syl3anc φ 0 0 1 N
41 1m1e0 1 1 = 0
42 41 oveq1i 1 1 N = 0 N
43 8 nncnd φ N
44 8 nnne0d φ N 0
45 43 44 div0d φ 0 N = 0
46 42 45 eqtrid φ 1 1 N = 0
47 46 oveq1d φ 1 1 N 1 N = 0 1 N
48 40 47 eleqtrrd φ 0 1 1 N 1 N
49 eqid 1 1 N 1 N = 1 1 N 1 N
50 simpr φ 1 1 N 1 1 N
51 1 2 3 4 5 6 7 8 9 10 11 12 49 cvmliftlem7 φ 1 1 N Q 1 1 1 1 N F -1 G 1 1 N
52 1 2 3 4 5 6 7 8 9 10 11 12 49 50 51 cvmliftlem6 φ 1 1 N Q 1 : 1 1 N 1 N B F Q 1 = G 1 1 N 1 N
53 23 52 mpdan φ Q 1 : 1 1 N 1 N B F Q 1 = G 1 1 N 1 N
54 53 simpld φ Q 1 : 1 1 N 1 N B
55 54 fdmd φ dom Q 1 = 1 1 N 1 N
56 48 55 eleqtrrd φ 0 dom Q 1
57 funssfv Fun K Q 1 K 0 dom Q 1 K 0 = Q 1 0
58 19 27 56 57 syl3anc φ K 0 = Q 1 0
59 1 2 3 4 5 6 7 8 9 10 11 12 cvmliftlem9 φ 1 1 N Q 1 1 1 N = Q 1 1 1 1 N
60 23 59 mpdan φ Q 1 1 1 N = Q 1 1 1 1 N
61 46 fveq2d φ Q 1 1 1 N = Q 1 0
62 41 fveq2i Q 1 1 = Q 0
63 1 2 3 4 5 6 7 8 9 10 11 12 cvmliftlem4 Q 0 = 0 P
64 62 63 eqtri Q 1 1 = 0 P
65 64 a1i φ Q 1 1 = 0 P
66 65 46 fveq12d φ Q 1 1 1 1 N = 0 P 0
67 60 61 66 3eqtr3d φ Q 1 0 = 0 P 0
68 0nn0 0 0
69 fvsng 0 0 P B 0 P 0 = P
70 68 6 69 sylancr φ 0 P 0 = P
71 58 67 70 3eqtrd φ K 0 = P