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=\bigcup J$$
	locfinbas.2	$$⊢Y=\bigcup A$$
Assertion	locfinbas	$$⊢A\in \mathrm{LocFin}\left(J\right)\to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		locfinbas.1	$$⊢X=\bigcup J$$
2		locfinbas.2	$$⊢Y=\bigcup A$$
3	1 2	islocfin	$$⊢A\in \mathrm{LocFin}\left(J\right)\leftrightarrow \left(J\in \mathrm{Top}\wedge X=Y\wedge \forall s\in X\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	simp2bi	$$⊢A\in \mathrm{LocFin}\left(J\right)\to X=Y$$