Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  locfincf Structured version   Unicode version

Theorem locfincf 20545
 Description: A locally finite cover in a coarser topology is locally finite in a finer topology. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
Hypothesis
Ref Expression
locfincf.1
Assertion
Ref Expression
locfincf TopOn

Proof of Theorem locfincf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 topontop 19940 . . . . 5 TopOn
21ad2antrr 730 . . . 4 TopOn
3 toponuni 19941 . . . . . 6 TopOn
43ad2antrr 730 . . . . 5 TopOn
5 locfincf.1 . . . . . . 7
6 eqid 2422 . . . . . . 7
75, 6locfinbas 20536 . . . . . 6
87adantl 467 . . . . 5 TopOn
94, 8eqtr3d 2465 . . . 4 TopOn
104eleq2d 2492 . . . . . 6 TopOn
115locfinnei 20537 . . . . . . . 8
1211ex 435 . . . . . . 7
13 ssrexv 3526 . . . . . . . 8
1413adantl 467 . . . . . . 7 TopOn
1512, 14sylan9r 662 . . . . . 6 TopOn
1610, 15sylbird 238 . . . . 5 TopOn
1716ralrimiv 2834 . . . 4 TopOn
18 eqid 2422 . . . . 5
1918, 6islocfin 20531 . . . 4
202, 9, 17, 19syl3anbrc 1189 . . 3 TopOn
2120ex 435 . 2 TopOn
2221ssrdv 3470 1 TopOn
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wceq 1437   wcel 1872   wne 2614  wral 2771  wrex 2772  crab 2775   cin 3435   wss 3436  c0 3761  cuni 4219  cfv 5601  cfn 7581  ctop 19916  TopOnctopon 19917  clocfin 20518 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fv 5609  df-top 19920  df-topon 19922  df-locfin 20521 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator