finlocfin

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

	Ref	Expression
Hypotheses	finlocfin.1	$⊢ X = ⋃ J$
	finlocfin.2	$⊢ Y = ⋃ A$
Assertion	finlocfin	$⊢ (J \in Top \land A \in Fin \land X = Y) \to A \in LocFin (J)$

Proof

Step	Hyp	Ref	Expression
1		finlocfin.1	$⊢ X = ⋃ J$
2		finlocfin.2	$⊢ Y = ⋃ A$
3		simp1	$⊢ (J \in Top \land A \in Fin \land X = Y) \to J \in Top$
4		simp3	$⊢ (J \in Top \land A \in Fin \land X = Y) \to X = Y$
5		simpl1	$⊢ ((J \in Top \land A \in Fin \land X = Y) \land x \in X) \to J \in Top$
6	1	topopn	$⊢ J \in Top \to X \in J$
7	5 6	syl	$⊢ ((J \in Top \land A \in Fin \land X = Y) \land x \in X) \to X \in J$
8		simpr	$⊢ ((J \in Top \land A \in Fin \land X = Y) \land x \in X) \to x \in X$
9		simpl2	$⊢ ((J \in Top \land A \in Fin \land X = Y) \land x \in X) \to A \in Fin$
10		ssrab2	$⊢ \{s \in A \| s \cap X \neq \emptyset\} \subseteq A$
11		ssfi	$⊢ (A \in Fin \land \{s \in A \| s \cap X \neq \emptyset\} \subseteq A) \to \{s \in A \| s \cap X \neq \emptyset\} \in Fin$
12	9 10 11	sylancl	$⊢ ((J \in Top \land A \in Fin \land X = Y) \land x \in X) \to \{s \in A \| s \cap X \neq \emptyset\} \in Fin$
13		eleq2	$⊢ n = X \to (x \in n \leftrightarrow x \in X)$
14		ineq2	$⊢ n = X \to s \cap n = s \cap X$
15	14	neeq1d	$⊢ n = X \to (s \cap n \neq \emptyset \leftrightarrow s \cap X \neq \emptyset)$
16	15	rabbidv	$⊢ n = X \to \{s \in A \| s \cap n \neq \emptyset\} = \{s \in A \| s \cap X \neq \emptyset\}$
17	16	eleq1d	$⊢ n = X \to (\{s \in A \| s \cap n \neq \emptyset\} \in Fin \leftrightarrow \{s \in A \| s \cap X \neq \emptyset\} \in Fin)$
18	13 17	anbi12d	$⊢ n = X \to ((x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin) \leftrightarrow (x \in X \land \{s \in A \| s \cap X \neq \emptyset\} \in Fin))$
19	18	rspcev	$⊢ (X \in J \land (x \in X \land \{s \in A \| s \cap X \neq \emptyset\} \in Fin)) \to \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$
20	7 8 12 19	syl12anc	$⊢ ((J \in Top \land A \in Fin \land X = Y) \land x \in X) \to \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$
21	20	ralrimiva	$⊢ (J \in Top \land A \in Fin \land X = Y) \to \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$
22	1 2	islocfin	$⊢ A \in LocFin (J) \leftrightarrow (J \in Top \land X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))$
23	3 4 21 22	syl3anbrc	$⊢ (J \in Top \land A \in Fin \land X = Y) \to A \in LocFin (J)$

Metamath Proof Explorer

Theorem finlocfin

Proof