dissnlocfin

Description: The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020)

		Ref	Expression
	Hypothesis	dissnref.c	$⊢ C = \{u \| \exists x \in X u = \{x\}\}$
	Assertion	dissnlocfin	$⊢ X \in V \to C \in LocFin (𝒫 X)$

Proof

Step	Hyp	Ref	Expression
1		dissnref.c	$⊢ C = \{u \| \exists x \in X u = \{x\}\}$
2		distop	$⊢ X \in V \to 𝒫 X \in Top$
3		eqidd	$⊢ X \in V \to X = X$
4		snelpwi	$⊢ z \in X \to \{z\} \in 𝒫 X$
5	4	adantl	$⊢ (X \in V \land z \in X) \to \{z\} \in 𝒫 X$
6		vsnid	$⊢ z \in \{z\}$
7	6	a1i	$⊢ (X \in V \land z \in X) \to z \in \{z\}$
8		nfv	$⊢ Ⅎ u (X \in V \land z \in X)$
9		nfrab1	$⊢ \underline{Ⅎ} u \{u \in C \| u \cap \{z\} \neq \emptyset\}$
10		nfcv	$⊢ \underline{Ⅎ} u \{\{z\}\}$
11	1	eqabri	$⊢ u \in C \leftrightarrow \exists x \in X u = \{x\}$
12	11	anbi1i	$⊢ (u \in C \land u \cap \{z\} \neq \emptyset) \leftrightarrow (\exists x \in X u = \{x\} \land u \cap \{z\} \neq \emptyset)$
13		simpr	$⊢ ((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \to u = \{x\}$
14		simplr	$⊢ (((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \land x \neq z) \to u = \{x\}$
15	14	ineq1d	$⊢ (((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \land x \neq z) \to u \cap \{z\} = \{x\} \cap \{z\}$
16		disjsn2	$⊢ x \neq z \to \{x\} \cap \{z\} = \emptyset$
17	16	adantl	$⊢ (((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \land x \neq z) \to \{x\} \cap \{z\} = \emptyset$
18	15 17	eqtrd	$⊢ (((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \land x \neq z) \to u \cap \{z\} = \emptyset$
19		simp-4r	$⊢ (((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \land x \neq z) \to u \cap \{z\} \neq \emptyset$
20	19	neneqd	$⊢ (((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \land x \neq z) \to \neg u \cap \{z\} = \emptyset$
21	18 20	pm2.65da	$⊢ ((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \to \neg x \neq z$
22		nne	$⊢ \neg x \neq z \leftrightarrow x = z$
23	21 22	sylib	$⊢ ((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \to x = z$
24	23	sneqd	$⊢ ((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \to \{x\} = \{z\}$
25	13 24	eqtrd	$⊢ ((((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land x \in X) \land u = \{x\}) \to u = \{z\}$
26	25	r19.29an	$⊢ (((X \in V \land z \in X) \land u \cap \{z\} \neq \emptyset) \land \exists x \in X u = \{x\}) \to u = \{z\}$
27	26	an32s	$⊢ (((X \in V \land z \in X) \land \exists x \in X u = \{x\}) \land u \cap \{z\} \neq \emptyset) \to u = \{z\}$
28	27	anasss	$⊢ ((X \in V \land z \in X) \land (\exists x \in X u = \{x\} \land u \cap \{z\} \neq \emptyset)) \to u = \{z\}$
29		sneq	$⊢ x = z \to \{x\} = \{z\}$
30	29	rspceeqv	$⊢ (z \in X \land u = \{z\}) \to \exists x \in X u = \{x\}$
31	30	adantll	$⊢ ((X \in V \land z \in X) \land u = \{z\}) \to \exists x \in X u = \{x\}$
32		simpr	$⊢ ((X \in V \land z \in X) \land u = \{z\}) \to u = \{z\}$
33	32	ineq1d	$⊢ ((X \in V \land z \in X) \land u = \{z\}) \to u \cap \{z\} = \{z\} \cap \{z\}$
34		inidm	$⊢ \{z\} \cap \{z\} = \{z\}$
35	33 34	eqtrdi	$⊢ ((X \in V \land z \in X) \land u = \{z\}) \to u \cap \{z\} = \{z\}$
36		vex	$⊢ z \in V$
37	36	snnz	$⊢ \{z\} \neq \emptyset$
38	37	a1i	$⊢ ((X \in V \land z \in X) \land u = \{z\}) \to \{z\} \neq \emptyset$
39	35 38	eqnetrd	$⊢ ((X \in V \land z \in X) \land u = \{z\}) \to u \cap \{z\} \neq \emptyset$
40	31 39	jca	$⊢ ((X \in V \land z \in X) \land u = \{z\}) \to (\exists x \in X u = \{x\} \land u \cap \{z\} \neq \emptyset)$
41	28 40	impbida	$⊢ (X \in V \land z \in X) \to ((\exists x \in X u = \{x\} \land u \cap \{z\} \neq \emptyset) \leftrightarrow u = \{z\})$
42	12 41	bitrid	$⊢ (X \in V \land z \in X) \to ((u \in C \land u \cap \{z\} \neq \emptyset) \leftrightarrow u = \{z\})$
43		rabid	$⊢ u \in \{u \in C \| u \cap \{z\} \neq \emptyset\} \leftrightarrow (u \in C \land u \cap \{z\} \neq \emptyset)$
44		velsn	$⊢ u \in \{\{z\}\} \leftrightarrow u = \{z\}$
45	42 43 44	3bitr4g	$⊢ (X \in V \land z \in X) \to (u \in \{u \in C \| u \cap \{z\} \neq \emptyset\} \leftrightarrow u \in \{\{z\}\})$
46	8 9 10 45	eqrd	$⊢ (X \in V \land z \in X) \to \{u \in C \| u \cap \{z\} \neq \emptyset\} = \{\{z\}\}$
47		snfi	$⊢ \{\{z\}\} \in Fin$
48	46 47	eqeltrdi	$⊢ (X \in V \land z \in X) \to \{u \in C \| u \cap \{z\} \neq \emptyset\} \in Fin$
49		eleq2	$⊢ y = \{z\} \to (z \in y \leftrightarrow z \in \{z\})$
50		ineq2	$⊢ y = \{z\} \to u \cap y = u \cap \{z\}$
51	50	neeq1d	$⊢ y = \{z\} \to (u \cap y \neq \emptyset \leftrightarrow u \cap \{z\} \neq \emptyset)$
52	51	rabbidv	$⊢ y = \{z\} \to \{u \in C \| u \cap y \neq \emptyset\} = \{u \in C \| u \cap \{z\} \neq \emptyset\}$
53	52	eleq1d	$⊢ y = \{z\} \to (\{u \in C \| u \cap y \neq \emptyset\} \in Fin \leftrightarrow \{u \in C \| u \cap \{z\} \neq \emptyset\} \in Fin)$
54	49 53	anbi12d	$⊢ y = \{z\} \to ((z \in y \land \{u \in C \| u \cap y \neq \emptyset\} \in Fin) \leftrightarrow (z \in \{z\} \land \{u \in C \| u \cap \{z\} \neq \emptyset\} \in Fin))$
55	54	rspcev	$⊢ (\{z\} \in 𝒫 X \land (z \in \{z\} \land \{u \in C \| u \cap \{z\} \neq \emptyset\} \in Fin)) \to \exists y \in 𝒫 X (z \in y \land \{u \in C \| u \cap y \neq \emptyset\} \in Fin)$
56	5 7 48 55	syl12anc	$⊢ (X \in V \land z \in X) \to \exists y \in 𝒫 X (z \in y \land \{u \in C \| u \cap y \neq \emptyset\} \in Fin)$
57	56	ralrimiva	$⊢ X \in V \to \forall z \in X \exists y \in 𝒫 X (z \in y \land \{u \in C \| u \cap y \neq \emptyset\} \in Fin)$
58		unipw	$⊢ ⋃ 𝒫 X = X$
59	58	eqcomi	$⊢ X = ⋃ 𝒫 X$
60	1	unisngl	$⊢ X = ⋃ C$
61	59 60	islocfin	$⊢ C \in LocFin (𝒫 X) \leftrightarrow (𝒫 X \in Top \land X = X \land \forall z \in X \exists y \in 𝒫 X (z \in y \land \{u \in C \| u \cap y \neq \emptyset\} \in Fin))$
62	2 3 57 61	syl3anbrc	$⊢ X \in V \to C \in LocFin (𝒫 X)$

Metamath Proof Explorer

Theorem dissnlocfin

Proof