This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem locfinnei

Description: A point covered by a locally finite cover has a neighborhood which intersects only finitely many elements of the cover. (Contributed by Jeff Hankins, 21-Jan-2010)

Ref Expression
Hypothesis locfinnei.1 ⊢ X = ⋃ J
Assertion locfinnei ⊢ A ∈ LocFin ⁡ J ∧ P ∈ X → ∃ n ∈ J P ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin

Proof

Step Hyp Ref Expression
1 locfinnei.1 ⊢ X = ⋃ J
2 eqid ⊢ ⋃ A = ⋃ A
3 1 2 islocfin ⊢ A ∈ LocFin ⁡ J ↔ J ∈ Top ∧ X = ⋃ A ∧ ∀ x ∈ X ∃ n ∈ J x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin
4 3 simp3bi ⊢ A ∈ LocFin ⁡ J → ∀ x ∈ X ∃ n ∈ J x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin
5 eleq1 ⊢ x = P → x ∈ n ↔ P ∈ n
6 5 anbi1d ⊢ x = P → x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin ↔ P ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin
7 6 rexbidv ⊢ x = P → ∃ n ∈ J x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin ↔ ∃ n ∈ J P ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin
8 7 rspccva ⊢ ∀ x ∈ X ∃ n ∈ J x ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin ∧ P ∈ X → ∃ n ∈ J P ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin
9 4 8 sylan ⊢ A ∈ LocFin ⁡ J ∧ P ∈ X → ∃ n ∈ J P ∈ n ∧ s ∈ A | s ∩ n ≠ ∅ ∈ Fin