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

Metamath Proof Explorer

Theorem locfinbas

Description: A locally finite cover must cover the base set of its corresponding topological space. (Contributed by Jeff Hankins, 21-Jan-2010)

Ref Expression
Hypotheses locfinbas.1 ⊢ 𝑋 = ∪ 𝐽
locfinbas.2 ⊢ 𝑌 = ∪ 𝐴
Assertion locfinbas ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → 𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 locfinbas.1 ⊢ 𝑋 = ∪ 𝐽
2 locfinbas.2 ⊢ 𝑌 = ∪ 𝐴
3 1 2 islocfin ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀ 𝑠 ∈ 𝑋 ∃ 𝑛 ∈ 𝐽 ( 𝑠 ∈ 𝑛 ∧ { 𝑥 ∈ 𝐴 ∣ ( 𝑥 ∩ 𝑛 ) ≠ ∅ } ∈ Fin ) ) )
4 3 simp2bi ⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → 𝑋 = 𝑌 )