Metamath Proof Explorer


Theorem cvmliftlem15

Description: Lemma for cvmlift . Discharge the assumptions of cvmliftlem14 . The set of all open subsets u of the unit interval such that G " u is contained in an even covering of some open set in J is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii , there is a subdivision of the closed unit interval into N equal parts such that each part is entirely contained within one such open set of J . Then using finite choice ac6sfi to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 . (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 S=kJs𝒫C|s=F-1kusvsuuv=FuC𝑡uHomeoJ𝑡k
cvmliftlem.b B=C
cvmliftlem.x X=J
cvmliftlem.f φFCCovMapJ
cvmliftlem.g φGIICnJ
cvmliftlem.p φPB
cvmliftlem.e φFP=G0
Assertion cvmliftlem15 φ∃!fIICnCFf=Gf0=P

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 S=kJs𝒫C|s=F-1kusvsuuv=FuC𝑡uHomeoJ𝑡k
2 cvmliftlem.b B=C
3 cvmliftlem.x X=J
4 cvmliftlem.f φFCCovMapJ
5 cvmliftlem.g φGIICnJ
6 cvmliftlem.p φPB
7 cvmliftlem.e φFP=G0
8 ssrab2 uII|jJsSjGujII
9 5 ad2antrr φx01jJGxjSjGIICnJ
10 simprl φx01jJGxjSjjJ
11 cnima GIICnJjJG-1jII
12 9 10 11 syl2anc φx01jJGxjSjG-1jII
13 simplr φx01jJGxjSjx01
14 simprrl φx01jJGxjSjGxj
15 iiuni 01=II
16 15 3 cnf GIICnJG:01X
17 5 16 syl φG:01X
18 17 ad2antrr φx01jJGxjSjG:01X
19 ffn G:01XGFn01
20 elpreima GFn01xG-1jx01Gxj
21 18 19 20 3syl φx01jJGxjSjxG-1jx01Gxj
22 13 14 21 mpbir2and φx01jJGxjSjxG-1j
23 simprrr φx01jJGxjSjSj
24 ffun G:01XFunG
25 funimacnv FunGGG-1j=jranG
26 18 24 25 3syl φx01jJGxjSjGG-1j=jranG
27 inss1 jranGj
28 26 27 eqsstrdi φx01jJGxjSjGG-1jj
29 28 ralrimivw φx01jJGxjSjsSjGG-1jj
30 r19.2z SjsSjGG-1jjsSjGG-1jj
31 23 29 30 syl2anc φx01jJGxjSjsSjGG-1jj
32 eleq2 u=G-1jxuxG-1j
33 imaeq2 u=G-1jGu=GG-1j
34 33 sseq1d u=G-1jGujGG-1jj
35 34 rexbidv u=G-1jsSjGujsSjGG-1jj
36 32 35 anbi12d u=G-1jxusSjGujxG-1jsSjGG-1jj
37 36 rspcev G-1jIIxG-1jsSjGG-1jjuIIxusSjGuj
38 12 22 31 37 syl12anc φx01jJGxjSjuIIxusSjGuj
39 4 adantr φx01FCCovMapJ
40 17 ffvelrnda φx01GxX
41 1 3 cvmcov FCCovMapJGxXjJGxjSj
42 39 40 41 syl2anc φx01jJGxjSj
43 38 42 reximddv φx01jJuIIxusSjGuj
44 r19.42v jJxusSjGujxujJsSjGuj
45 44 rexbii uIIjJxusSjGujuIIxujJsSjGuj
46 rexcom jJuIIxusSjGujuIIjJxusSjGuj
47 elunirab xuII|jJsSjGujuIIxujJsSjGuj
48 45 46 47 3bitr4i jJuIIxusSjGujxuII|jJsSjGuj
49 43 48 sylib φx01xuII|jJsSjGuj
50 49 ex φx01xuII|jJsSjGuj
51 50 ssrdv φ01uII|jJsSjGuj
52 uniss uII|jJsSjGujIIuII|jJsSjGujII
53 8 52 mp1i φuII|jJsSjGujII
54 53 15 sseqtrrdi φuII|jJsSjGuj01
55 51 54 eqssd φ01=uII|jJsSjGuj
56 lebnumii uII|jJsSjGujII01=uII|jJsSjGujnk1nvuII|jJsSjGujk1nknv
57 8 55 56 sylancr φnk1nvuII|jJsSjGujk1nknv
58 fzfi 1nFin
59 imaeq2 u=vGu=Gv
60 59 sseq1d u=vGujGvj
61 60 2rexbidv u=vjJsSjGujjJsSjGvj
62 61 rexrab vuII|jJsSjGujk1nknvvIIjJsSjGvjk1nknv
63 vex jV
64 vex sV
65 63 64 op1std u=js1stu=j
66 65 sseq2d u=jsGv1stuGvj
67 66 rexiunxp ujJj×SjGv1stujJsSjGvj
68 imass2 k1nknvGk1nknGv
69 sstr2 Gk1nknGvGv1stuGk1nkn1stu
70 68 69 syl k1nknvGv1stuGk1nkn1stu
71 70 reximdv k1nknvujJj×SjGv1stuujJj×SjGk1nkn1stu
72 67 71 syl5bir k1nknvjJsSjGvjujJj×SjGk1nkn1stu
73 72 impcom jJsSjGvjk1nknvujJj×SjGk1nkn1stu
74 73 rexlimivw vIIjJsSjGvjk1nknvujJj×SjGk1nkn1stu
75 62 74 sylbi vuII|jJsSjGujk1nknvujJj×SjGk1nkn1stu
76 75 ralimi k1nvuII|jJsSjGujk1nknvk1nujJj×SjGk1nkn1stu
77 fveq2 u=gk1stu=1stgk
78 77 sseq2d u=gkGk1nkn1stuGk1nkn1stgk
79 78 ac6sfi 1nFink1nujJj×SjGk1nkn1stugg:1njJj×Sjk1nGk1nkn1stgk
80 58 76 79 sylancr k1nvuII|jJsSjGujk1nknvgg:1njJj×Sjk1nGk1nkn1stgk
81 4 ad2antrr φng:1njJj×Sjk1nGk1nkn1stgkFCCovMapJ
82 5 ad2antrr φng:1njJj×Sjk1nGk1nkn1stgkGIICnJ
83 6 ad2antrr φng:1njJj×Sjk1nGk1nkn1stgkPB
84 7 ad2antrr φng:1njJj×Sjk1nGk1nkn1stgkFP=G0
85 simplr φng:1njJj×Sjk1nGk1nkn1stgkn
86 simprl φng:1njJj×Sjk1nGk1nkn1stgkg:1njJj×Sj
87 sneq j=aj=a
88 fveq2 j=aSj=Sa
89 87 88 xpeq12d j=aj×Sj=a×Sa
90 89 cbviunv jJj×Sj=aJa×Sa
91 feq3 jJj×Sj=aJa×Sag:1njJj×Sjg:1naJa×Sa
92 90 91 ax-mp g:1njJj×Sjg:1naJa×Sa
93 86 92 sylib φng:1njJj×Sjk1nGk1nkn1stgkg:1naJa×Sa
94 simprr φng:1njJj×Sjk1nGk1nkn1stgkk1nGk1nkn1stgk
95 eqid topGenran.=topGenran.
96 2fveq3 t=zFιc2ndgw|yw1nc-1Gt=Fιc2ndgw|yw1nc-1Gz
97 96 cbvmptv tw1nwnFιc2ndgw|yw1nc-1Gt=zw1nwnFιc2ndgw|yw1nc-1Gz
98 eleq2 c=byw1ncyw1nb
99 98 cbvriotavw ιc2ndgw|yw1nc=ιb2ndgw|yw1nb
100 fveq1 y=xyw1n=xw1n
101 100 eleq1d y=xyw1nbxw1nb
102 101 riotabidv y=xιb2ndgw|yw1nb=ιb2ndgw|xw1nb
103 99 102 eqtrid y=xιc2ndgw|yw1nc=ιb2ndgw|xw1nb
104 103 reseq2d y=xFιc2ndgw|yw1nc=Fιb2ndgw|xw1nb
105 104 cnveqd y=xFιc2ndgw|yw1nc-1=Fιb2ndgw|xw1nb-1
106 105 fveq1d y=xFιc2ndgw|yw1nc-1Gz=Fιb2ndgw|xw1nb-1Gz
107 106 mpteq2dv y=xzw1nwnFιc2ndgw|yw1nc-1Gz=zw1nwnFιb2ndgw|xw1nb-1Gz
108 97 107 eqtrid y=xtw1nwnFιc2ndgw|yw1nc-1Gt=zw1nwnFιb2ndgw|xw1nb-1Gz
109 oveq1 w=mw1=m1
110 109 oveq1d w=mw1n=m1n
111 oveq1 w=mwn=mn
112 110 111 oveq12d w=mw1nwn=m1nmn
113 2fveq3 w=m2ndgw=2ndgm
114 110 fveq2d w=mxw1n=xm1n
115 114 eleq1d w=mxw1nbxm1nb
116 113 115 riotaeqbidv w=mιb2ndgw|xw1nb=ιb2ndgm|xm1nb
117 116 reseq2d w=mFιb2ndgw|xw1nb=Fιb2ndgm|xm1nb
118 117 cnveqd w=mFιb2ndgw|xw1nb-1=Fιb2ndgm|xm1nb-1
119 118 fveq1d w=mFιb2ndgw|xw1nb-1Gz=Fιb2ndgm|xm1nb-1Gz
120 112 119 mpteq12dv w=mzw1nwnFιb2ndgw|xw1nb-1Gz=zm1nmnFιb2ndgm|xm1nb-1Gz
121 108 120 cbvmpov yV,wtw1nwnFιc2ndgw|yw1nc-1Gt=xV,mzm1nmnFιb2ndgm|xm1nb-1Gz
122 seqeq2 yV,wtw1nwnFιc2ndgw|yw1nc-1Gt=xV,mzm1nmnFιb2ndgm|xm1nb-1Gzseq0yV,wtw1nwnFιc2ndgw|yw1nc-1GtI00P=seq0xV,mzm1nmnFιb2ndgm|xm1nb-1GzI00P
123 121 122 ax-mp seq0yV,wtw1nwnFιc2ndgw|yw1nc-1GtI00P=seq0xV,mzm1nmnFιb2ndgm|xm1nb-1GzI00P
124 eqid k=1nseq0yV,wtw1nwnFιc2ndgw|yw1nc-1GtI00Pk=k=1nseq0yV,wtw1nwnFιc2ndgw|yw1nc-1GtI00Pk
125 1 2 3 81 82 83 84 85 93 94 95 123 124 cvmliftlem14 φng:1njJj×Sjk1nGk1nkn1stgk∃!fIICnCFf=Gf0=P
126 125 ex φng:1njJj×Sjk1nGk1nkn1stgk∃!fIICnCFf=Gf0=P
127 126 exlimdv φngg:1njJj×Sjk1nGk1nkn1stgk∃!fIICnCFf=Gf0=P
128 80 127 syl5 φnk1nvuII|jJsSjGujk1nknv∃!fIICnCFf=Gf0=P
129 128 rexlimdva φnk1nvuII|jJsSjGujk1nknv∃!fIICnCFf=Gf0=P
130 57 129 mpd φ∃!fIICnCFf=Gf0=P