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 ⊢ 𝑋 = ∪ 𝐽
Assertion locfinnei ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 locfinnei.1 ⊢ 𝑋 = ∪ 𝐽
2 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
3 1 2 islocfin ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
4 3 simp3bi ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
5 eleq1 ⊢ ( 𝑥 = 𝑃 → ( 𝑥 ∈ 𝑛 ↔ 𝑃 ∈ 𝑛 ) )
6 5 anbi1d ⊢ ( 𝑥 = 𝑃 → ( ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ↔ ( 𝑃 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
7 6 rexbidv ⊢ ( 𝑥 = 𝑃 → ( ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ↔ ∃ 𝑛 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
8 7 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )
9 4 8 sylan ⊢ ( ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ { 𝑠 ∈ 𝐴 ∣ ( 𝑠 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) )