dispcmp

Description: Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020)

		Ref	Expression
	Assertion	dispcmp	$⊢ X \in V \to 𝒫 X \in Paracomp$

Proof

Step	Hyp	Ref	Expression
1		distop	$⊢ X \in V \to 𝒫 X \in Top$
2		simpr	$⊢ (x \in X \land u = \{x\}) \to u = \{x\}$
3		snelpwi	$⊢ x \in X \to \{x\} \in 𝒫 X$
4	3	adantr	$⊢ (x \in X \land u = \{x\}) \to \{x\} \in 𝒫 X$
5	2 4	eqeltrd	$⊢ (x \in X \land u = \{x\}) \to u \in 𝒫 X$
6	5	rexlimiva	$⊢ \exists x \in X u = \{x\} \to u \in 𝒫 X$
7	6	abssi	$⊢ \{u \| \exists x \in X u = \{x\}\} \subseteq 𝒫 X$
8		simpl	$⊢ (u = v \land x = z) \to u = v$
9		simpr	$⊢ (u = v \land x = z) \to x = z$
10	9	sneqd	$⊢ (u = v \land x = z) \to \{x\} = \{z\}$
11	8 10	eqeq12d	$⊢ (u = v \land x = z) \to (u = \{x\} \leftrightarrow v = \{z\})$
12	11	cbvrexdva	$⊢ u = v \to (\exists x \in X u = \{x\} \leftrightarrow \exists z \in X v = \{z\})$
13	12	cbvabv	$⊢ \{u \| \exists x \in X u = \{x\}\} = \{v \| \exists z \in X v = \{z\}\}$
14	13	dissnlocfin	$⊢ X \in V \to \{u \| \exists x \in X u = \{x\}\} \in LocFin (𝒫 X)$
15		elpwg	$⊢ \{u \| \exists x \in X u = \{x\}\} \in LocFin (𝒫 X) \to (\{u \| \exists x \in X u = \{x\}\} \in 𝒫 𝒫 X \leftrightarrow \{u \| \exists x \in X u = \{x\}\} \subseteq 𝒫 X)$
16	14 15	syl	$⊢ X \in V \to (\{u \| \exists x \in X u = \{x\}\} \in 𝒫 𝒫 X \leftrightarrow \{u \| \exists x \in X u = \{x\}\} \subseteq 𝒫 X)$
17	7 16	mpbiri	$⊢ X \in V \to \{u \| \exists x \in X u = \{x\}\} \in 𝒫 𝒫 X$
18	17	ad2antrr	$⊢ ((X \in V \land y \in 𝒫 𝒫 X) \land X = ⋃ y) \to \{u \| \exists x \in X u = \{x\}\} \in 𝒫 𝒫 X$
19	14	ad2antrr	$⊢ ((X \in V \land y \in 𝒫 𝒫 X) \land X = ⋃ y) \to \{u \| \exists x \in X u = \{x\}\} \in LocFin (𝒫 X)$
20	18 19	elind	$⊢ ((X \in V \land y \in 𝒫 𝒫 X) \land X = ⋃ y) \to \{u \| \exists x \in X u = \{x\}\} \in (𝒫 𝒫 X \cap LocFin (𝒫 X))$
21		simpll	$⊢ ((X \in V \land y \in 𝒫 𝒫 X) \land X = ⋃ y) \to X \in V$
22		simpr	$⊢ ((X \in V \land y \in 𝒫 𝒫 X) \land X = ⋃ y) \to X = ⋃ y$
23	22	eqcomd	$⊢ ((X \in V \land y \in 𝒫 𝒫 X) \land X = ⋃ y) \to ⋃ y = X$
24	13	dissnref	$⊢ (X \in V \land ⋃ y = X) \to \{u \| \exists x \in X u = \{x\}\} Ref y$
25	21 23 24	syl2anc	$⊢ ((X \in V \land y \in 𝒫 𝒫 X) \land X = ⋃ y) \to \{u \| \exists x \in X u = \{x\}\} Ref y$
26		breq1	$⊢ z = \{u \| \exists x \in X u = \{x\}\} \to (z Ref y \leftrightarrow \{u \| \exists x \in X u = \{x\}\} Ref y)$
27	26	rspcev	$⊢ (\{u \| \exists x \in X u = \{x\}\} \in (𝒫 𝒫 X \cap LocFin (𝒫 X)) \land \{u \| \exists x \in X u = \{x\}\} Ref y) \to \exists z \in (𝒫 𝒫 X \cap LocFin (𝒫 X)) z Ref y$
28	20 25 27	syl2anc	$⊢ ((X \in V \land y \in 𝒫 𝒫 X) \land X = ⋃ y) \to \exists z \in (𝒫 𝒫 X \cap LocFin (𝒫 X)) z Ref y$
29	28	ex	$⊢ (X \in V \land y \in 𝒫 𝒫 X) \to (X = ⋃ y \to \exists z \in (𝒫 𝒫 X \cap LocFin (𝒫 X)) z Ref y)$
30	29	ralrimiva	$⊢ X \in V \to \forall y \in 𝒫 𝒫 X (X = ⋃ y \to \exists z \in (𝒫 𝒫 X \cap LocFin (𝒫 X)) z Ref y)$
31		unipw	$⊢ ⋃ 𝒫 X = X$
32	31	eqcomi	$⊢ X = ⋃ 𝒫 X$
33	32	iscref	$⊢ 𝒫 X \in CovHasRef LocFin (𝒫 X) \leftrightarrow (𝒫 X \in Top \land \forall y \in 𝒫 𝒫 X (X = ⋃ y \to \exists z \in (𝒫 𝒫 X \cap LocFin (𝒫 X)) z Ref y))$
34	1 30 33	sylanbrc	$⊢ X \in V \to 𝒫 X \in CovHasRef LocFin (𝒫 X)$
35		ispcmp	$⊢ 𝒫 X \in Paracomp \leftrightarrow 𝒫 X \in CovHasRef LocFin (𝒫 X)$
36	34 35	sylibr	$⊢ X \in V \to 𝒫 X \in Paracomp$

Metamath Proof Explorer

Theorem dispcmp

Proof