Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftlem1 Unicode version

Theorem cvmliftlem1 24100
 Description: Lemma for cvmlift 24114. In cvmliftlem15 24113, we picked an large enough so that the sections are all contained in an even covering, and the function enumerates these even coverings. So is a neighborhood of , and is an even covering of , which is to say a disjoint union of open sets in whose image is . (Contributed by Mario Carneiro, 14-Feb-2015.)
Hypotheses
Ref Expression
cvmliftlem.1 t t
cvmliftlem.b
cvmliftlem.x
cvmliftlem.f CovMap
cvmliftlem.g
cvmliftlem.p
cvmliftlem.e
cvmliftlem.n
cvmliftlem.t
cvmliftlem.a
cvmliftlem.l
cvmliftlem1.m
Assertion
Ref Expression
cvmliftlem1
Distinct variable groups:   ,   ,,,,,   ,,,,,   ,,,   ,,,,,   ,,   ,,,   ,,,,,   ,   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   (,,)   (,,,,)   (,,,)   (,)   (,,,,)   (,)   (,,,)

Proof of Theorem cvmliftlem1
StepHypRef Expression
1 relxp 4831 . . . . . 6
21rgenw 2644 . . . . 5
3 reliun 4843 . . . . 5
42, 3mpbir 200 . . . 4
5 cvmliftlem.t . . . . . 6
65adantr 451 . . . . 5
7 cvmliftlem1.m . . . . 5
8 ffvelrn 5701 . . . . 5
96, 7, 8syl2anc 642 . . . 4
10 1st2nd 6208 . . . 4
114, 9, 10sylancr 644 . . 3
1211, 9eqeltrrd 2391 . 2
13 fveq2 5563 . . . 4
1413opeliunxp2 4861 . . 3
1514simprbi 450 . 2
1612, 15syl 15 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   wceq 1633   wcel 1701  wral 2577  crab 2581   cdif 3183   cin 3185   wss 3186  c0 3489  cpw 3659  csn 3674  cop 3677  cuni 3864  ciun 3942   cmpt 4114   cxp 4724  ccnv 4725   crn 4727   cres 4728  cima 4729   wrel 4731  wf 5288  cfv 5292  (class class class)co 5900  c1st 6162  c2nd 6163  cc0 8782  c1 8783   cmin 9082   cdiv 9468  cn 9791  cioo 10703  cicc 10706  cfz 10829   ↾t crest 13374  ctg 13391   ccn 17010   chmeo 17500  cii 18431   CovMap ccvm 24070 This theorem is referenced by:  cvmliftlem6  24105  cvmliftlem8  24107  cvmliftlem9  24108 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-fv 5300  df-1st 6164  df-2nd 6165
 Copyright terms: Public domain W3C validator