Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  finlocfin Structured version   Visualization version   GIF version

Theorem finlocfin 22220
 Description: A finite cover of a topological space is a locally finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.)
Hypotheses
Ref Expression
finlocfin.1 𝑋 = 𝐽
finlocfin.2 𝑌 = 𝐴
Assertion
Ref Expression
finlocfin ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐴 ∈ (LocFin‘𝐽))

Proof of Theorem finlocfin
Dummy variables 𝑛 𝑠 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 1133 . 2 ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐽 ∈ Top)
2 simp3 1135 . 2 ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) → 𝑋 = 𝑌)
3 simpl1 1188 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) ∧ 𝑥𝑋) → 𝐽 ∈ Top)
4 finlocfin.1 . . . . . 6 𝑋 = 𝐽
54topopn 21606 . . . . 5 (𝐽 ∈ Top → 𝑋𝐽)
63, 5syl 17 . . . 4 (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) ∧ 𝑥𝑋) → 𝑋𝐽)
7 simpr 488 . . . 4 (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) ∧ 𝑥𝑋) → 𝑥𝑋)
8 simpl2 1189 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) ∧ 𝑥𝑋) → 𝐴 ∈ Fin)
9 ssrab2 3984 . . . . 5 {𝑠𝐴 ∣ (𝑠𝑋) ≠ ∅} ⊆ 𝐴
10 ssfi 8742 . . . . 5 ((𝐴 ∈ Fin ∧ {𝑠𝐴 ∣ (𝑠𝑋) ≠ ∅} ⊆ 𝐴) → {𝑠𝐴 ∣ (𝑠𝑋) ≠ ∅} ∈ Fin)
118, 9, 10sylancl 589 . . . 4 (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) ∧ 𝑥𝑋) → {𝑠𝐴 ∣ (𝑠𝑋) ≠ ∅} ∈ Fin)
12 eleq2 2840 . . . . . 6 (𝑛 = 𝑋 → (𝑥𝑛𝑥𝑋))
13 ineq2 4111 . . . . . . . . 9 (𝑛 = 𝑋 → (𝑠𝑛) = (𝑠𝑋))
1413neeq1d 3010 . . . . . . . 8 (𝑛 = 𝑋 → ((𝑠𝑛) ≠ ∅ ↔ (𝑠𝑋) ≠ ∅))
1514rabbidv 3392 . . . . . . 7 (𝑛 = 𝑋 → {𝑠𝐴 ∣ (𝑠𝑛) ≠ ∅} = {𝑠𝐴 ∣ (𝑠𝑋) ≠ ∅})
1615eleq1d 2836 . . . . . 6 (𝑛 = 𝑋 → ({𝑠𝐴 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin ↔ {𝑠𝐴 ∣ (𝑠𝑋) ≠ ∅} ∈ Fin))
1712, 16anbi12d 633 . . . . 5 (𝑛 = 𝑋 → ((𝑥𝑛 ∧ {𝑠𝐴 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin) ↔ (𝑥𝑋 ∧ {𝑠𝐴 ∣ (𝑠𝑋) ≠ ∅} ∈ Fin)))
1817rspcev 3541 . . . 4 ((𝑋𝐽 ∧ (𝑥𝑋 ∧ {𝑠𝐴 ∣ (𝑠𝑋) ≠ ∅} ∈ Fin)) → ∃𝑛𝐽 (𝑥𝑛 ∧ {𝑠𝐴 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin))
196, 7, 11, 18syl12anc 835 . . 3 (((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) ∧ 𝑥𝑋) → ∃𝑛𝐽 (𝑥𝑛 ∧ {𝑠𝐴 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin))
2019ralrimiva 3113 . 2 ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) → ∀𝑥𝑋𝑛𝐽 (𝑥𝑛 ∧ {𝑠𝐴 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin))
21 finlocfin.2 . . 3 𝑌 = 𝐴
224, 21islocfin 22217 . 2 (𝐴 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥𝑋𝑛𝐽 (𝑥𝑛 ∧ {𝑠𝐴 ∣ (𝑠𝑛) ≠ ∅} ∈ Fin)))
231, 2, 20, 22syl3anbrc 1340 1 ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐴 ∈ (LocFin‘𝐽))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  {crab 3074   ∩ cin 3857   ⊆ wss 3858  ∅c0 4225  ∪ cuni 4798  ‘cfv 6335  Fincfn 8527  Topctop 21593  LocFinclocfin 22204 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-om 7580  df-1o 8112  df-en 8528  df-fin 8531  df-top 21594  df-locfin 22207 This theorem is referenced by:  locfincmp  22226  cmppcmp  31329
 Copyright terms: Public domain W3C validator