Metamath Proof Explorer

Theorem locfinnei

Description: A point covered by a locally finite cover has a neighborhood which intersects only finitely many elements of the cover. (Contributed by Jeff Hankins, 21-Jan-2010)

		Ref	Expression
	Hypothesis	locfinnei.1	$⊢ X = ⋃ J$
	Assertion	locfinnei	$⊢ (A \in LocFin (J) \land P \in X) \to \exists n \in J (P \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$

Proof

Step	Hyp	Ref	Expression
1		locfinnei.1	$⊢ X = ⋃ J$
2		eqid	$⊢ ⋃ A = ⋃ A$
3	1 2	islocfin	$⊢ A \in LocFin (J) \leftrightarrow (J \in Top \land X = ⋃ A \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))$
4	3	simp3bi	$⊢ A \in LocFin (J) \to \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$
5		eleq1	$⊢ x = P \to (x \in n \leftrightarrow P \in n)$
6	5	anbi1d	$⊢ x = P \to ((x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin) \leftrightarrow (P \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))$
7	6	rexbidv	$⊢ x = P \to (\exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin) \leftrightarrow \exists n \in J (P \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))$
8	7	rspccva	$⊢ (\forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin) \land P \in X) \to \exists n \in J (P \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$
9	4 8	sylan	$⊢ (A \in LocFin (J) \land P \in X) \to \exists n \in J (P \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$