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 ) )