Theorem locfintop

Description: A locally finite cover covers a topological space. (Contributed by Jeff Hankins, 21-Jan-2010)

	Ref	Expression
Assertion	locfintop	⊢ ( 𝐴 ∈ ( LocFin ‘ 𝐽 ) → 𝐽 ∈ Top )

Proof

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