Theorem locfintop

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

	Ref	Expression
Assertion	locfintop	$$⊢A\in \mathrm{LocFin}\left(J\right)\to J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2		eqid	$$⊢\bigcup A=\bigcup A$$
3	1 2	islocfin	$$⊢A\in \mathrm{LocFin}\left(J\right)\leftrightarrow \left(J\in \mathrm{Top}\wedge \bigcup J=\bigcup A\wedge \forall s\in \bigcup J\exists n\in J\left(s\in n\wedge \left\{x\in A|x\cap n\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)$$
4	3	simp1bi	$$⊢A\in \mathrm{LocFin}\left(J\right)\to J\in \mathrm{Top}$$