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 ⊢ X = ⋃ J
locfinbas.2 ⊢ Y = ⋃ A
Assertion locfinbas ⊢ A ∈ LocFin ⁡ J → X = Y

Proof

Step Hyp Ref Expression
1 locfinbas.1 ⊢ X = ⋃ J
2 locfinbas.2 ⊢ Y = ⋃ A
3 1 2 islocfin ⊢ A ∈ LocFin ⁡ J ↔ J ∈ Top ∧ X = Y ∧ ∀ s ∈ X ∃ n ∈ J s ∈ n ∧ x ∈ A | x ∩ n ≠ ∅ ∈ Fin
4 3 simp2bi ⊢ A ∈ LocFin ⁡ J → X = Y