Metamath Proof Explorer


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 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 .
cvmliftlem1.m φ ψ M 1 N
Assertion cvmliftlem1 φ ψ 2 nd T M S 1 st T M

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 cvmliftlem1.m φ ψ M 1 N
13 relxp Rel j × S j
14 13 rgenw j J Rel j × S j
15 reliun Rel j J j × S j j J Rel j × S j
16 14 15 mpbir Rel j J j × S j
17 9 adantr φ ψ T : 1 N j J j × S j
18 17 12 ffvelrnd φ ψ T M j J j × S j
19 1st2nd Rel j J j × S j T M j J j × S j T M = 1 st T M 2 nd T M
20 16 18 19 sylancr φ ψ T M = 1 st T M 2 nd T M
21 20 18 eqeltrrd φ ψ 1 st T M 2 nd T M j J j × S j
22 fveq2 j = 1 st T M S j = S 1 st T M
23 22 opeliunxp2 1 st T M 2 nd T M j J j × S j 1 st T M J 2 nd T M S 1 st T M
24 23 simprbi 1 st T M 2 nd T M j J j × S j 2 nd T M S 1 st T M
25 21 24 syl φ ψ 2 nd T M S 1 st T M