locfindis

Description: The locally finite covers of a discrete space are precisely the point-finite covers. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Hypothesis	locfindis.1	$⊢ Y = ⋃ C$
	Assertion	locfindis	$⊢ C \in LocFin (𝒫 X) \leftrightarrow (C \in PtFin \land X = Y)$

Proof

Step	Hyp	Ref	Expression
1		locfindis.1	$⊢ Y = ⋃ C$
2		lfinpfin	$⊢ C \in LocFin (𝒫 X) \to C \in PtFin$
3		unipw	$⊢ ⋃ 𝒫 X = X$
4	3	eqcomi	$⊢ X = ⋃ 𝒫 X$
5	4 1	locfinbas	$⊢ C \in LocFin (𝒫 X) \to X = Y$
6	2 5	jca	$⊢ C \in LocFin (𝒫 X) \to (C \in PtFin \land X = Y)$
7		simpr	$⊢ (C \in PtFin \land X = Y) \to X = Y$
8		uniexg	$⊢ C \in PtFin \to ⋃ C \in V$
9	1 8	eqeltrid	$⊢ C \in PtFin \to Y \in V$
10	9	adantr	$⊢ (C \in PtFin \land X = Y) \to Y \in V$
11	7 10	eqeltrd	$⊢ (C \in PtFin \land X = Y) \to X \in V$
12		distop	$⊢ X \in V \to 𝒫 X \in Top$
13	11 12	syl	$⊢ (C \in PtFin \land X = Y) \to 𝒫 X \in Top$
14		snelpwi	$⊢ x \in X \to \{x\} \in 𝒫 X$
15	14	adantl	$⊢ ((C \in PtFin \land X = Y) \land x \in X) \to \{x\} \in 𝒫 X$
16		snidg	$⊢ x \in X \to x \in \{x\}$
17	16	adantl	$⊢ ((C \in PtFin \land X = Y) \land x \in X) \to x \in \{x\}$
18		simpll	$⊢ ((C \in PtFin \land X = Y) \land x \in X) \to C \in PtFin$
19	7	eleq2d	$⊢ (C \in PtFin \land X = Y) \to (x \in X \leftrightarrow x \in Y)$
20	19	biimpa	$⊢ ((C \in PtFin \land X = Y) \land x \in X) \to x \in Y$
21	1	ptfinfin	$⊢ (C \in PtFin \land x \in Y) \to \{s \in C \| x \in s\} \in Fin$
22	18 20 21	syl2anc	$⊢ ((C \in PtFin \land X = Y) \land x \in X) \to \{s \in C \| x \in s\} \in Fin$
23		eleq2	$⊢ y = \{x\} \to (x \in y \leftrightarrow x \in \{x\})$
24		ineq2	$⊢ y = \{x\} \to s \cap y = s \cap \{x\}$
25	24	neeq1d	$⊢ y = \{x\} \to (s \cap y \neq \emptyset \leftrightarrow s \cap \{x\} \neq \emptyset)$
26		disjsn	$⊢ s \cap \{x\} = \emptyset \leftrightarrow \neg x \in s$
27	26	necon2abii	$⊢ x \in s \leftrightarrow s \cap \{x\} \neq \emptyset$
28	25 27	bitr4di	$⊢ y = \{x\} \to (s \cap y \neq \emptyset \leftrightarrow x \in s)$
29	28	rabbidv	$⊢ y = \{x\} \to \{s \in C \| s \cap y \neq \emptyset\} = \{s \in C \| x \in s\}$
30	29	eleq1d	$⊢ y = \{x\} \to (\{s \in C \| s \cap y \neq \emptyset\} \in Fin \leftrightarrow \{s \in C \| x \in s\} \in Fin)$
31	23 30	anbi12d	$⊢ y = \{x\} \to ((x \in y \land \{s \in C \| s \cap y \neq \emptyset\} \in Fin) \leftrightarrow (x \in \{x\} \land \{s \in C \| x \in s\} \in Fin))$
32	31	rspcev	$⊢ (\{x\} \in 𝒫 X \land (x \in \{x\} \land \{s \in C \| x \in s\} \in Fin)) \to \exists y \in 𝒫 X (x \in y \land \{s \in C \| s \cap y \neq \emptyset\} \in Fin)$
33	15 17 22 32	syl12anc	$⊢ ((C \in PtFin \land X = Y) \land x \in X) \to \exists y \in 𝒫 X (x \in y \land \{s \in C \| s \cap y \neq \emptyset\} \in Fin)$
34	33	ralrimiva	$⊢ (C \in PtFin \land X = Y) \to \forall x \in X \exists y \in 𝒫 X (x \in y \land \{s \in C \| s \cap y \neq \emptyset\} \in Fin)$
35	4 1	islocfin	$⊢ C \in LocFin (𝒫 X) \leftrightarrow (𝒫 X \in Top \land X = Y \land \forall x \in X \exists y \in 𝒫 X (x \in y \land \{s \in C \| s \cap y \neq \emptyset\} \in Fin))$
36	13 7 34 35	syl3anbrc	$⊢ (C \in PtFin \land X = Y) \to C \in LocFin (𝒫 X)$
37	6 36	impbii	$⊢ C \in LocFin (𝒫 X) \leftrightarrow (C \in PtFin \land X = Y)$

Metamath Proof Explorer

Theorem locfindis

Proof