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 ‘ 𝐽 ) → 𝑋 = 𝑌 )