cmppcmp

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

		Ref	Expression
	Assertion	cmppcmp	$⊢ J \in Comp \to J \in Paracomp$

Proof

Step	Hyp	Ref	Expression
1		cmptop	$⊢ J \in Comp \to J \in Top$
2		cmpcref	$⊢ Comp = CovHasRef Fin$
3	2	eleq2i	$⊢ J \in Comp \leftrightarrow J \in CovHasRef Fin$
4		eqid	$⊢ ⋃ J = ⋃ J$
5	4	iscref	$⊢ J \in CovHasRef Fin \leftrightarrow (J \in Top \land \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap Fin) z Ref y))$
6	3 5	bitri	$⊢ J \in Comp \leftrightarrow (J \in Top \land \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap Fin) z Ref y))$
7	6	simprbi	$⊢ J \in Comp \to \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap Fin) z Ref y)$
8		simprl	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to z \in (𝒫 J \cap Fin)$
9		elin	$⊢ z \in (𝒫 J \cap Fin) \leftrightarrow (z \in 𝒫 J \land z \in Fin)$
10	8 9	sylib	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to (z \in 𝒫 J \land z \in Fin)$
11	10	simpld	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to z \in 𝒫 J$
12	1	ad3antrrr	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to J \in Top$
13	10	simprd	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to z \in Fin$
14		simplr	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to ⋃ J = ⋃ y$
15		simprr	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to z Ref y$
16		eqid	$⊢ ⋃ z = ⋃ z$
17		eqid	$⊢ ⋃ y = ⋃ y$
18	16 17	refbas	$⊢ z Ref y \to ⋃ y = ⋃ z$
19	15 18	syl	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to ⋃ y = ⋃ z$
20	14 19	eqtrd	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to ⋃ J = ⋃ z$
21	4 16	finlocfin	$⊢ (J \in Top \land z \in Fin \land ⋃ J = ⋃ z) \to z \in LocFin (J)$
22	12 13 20 21	syl3anc	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to z \in LocFin (J)$
23	11 22	elind	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to z \in (𝒫 J \cap LocFin (J))$
24	23 15	jca	$⊢ (((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \land (z \in (𝒫 J \cap Fin) \land z Ref y)) \to (z \in (𝒫 J \cap LocFin (J)) \land z Ref y)$
25	24	ex	$⊢ ((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \to ((z \in (𝒫 J \cap Fin) \land z Ref y) \to (z \in (𝒫 J \cap LocFin (J)) \land z Ref y))$
26	25	reximdv2	$⊢ ((J \in Comp \land y \in 𝒫 J) \land ⋃ J = ⋃ y) \to (\exists z \in (𝒫 J \cap Fin) z Ref y \to \exists z \in (𝒫 J \cap LocFin (J)) z Ref y)$
27	26	ex	$⊢ (J \in Comp \land y \in 𝒫 J) \to (⋃ J = ⋃ y \to (\exists z \in (𝒫 J \cap Fin) z Ref y \to \exists z \in (𝒫 J \cap LocFin (J)) z Ref y))$
28	27	a2d	$⊢ (J \in Comp \land y \in 𝒫 J) \to ((⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap Fin) z Ref y) \to (⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap LocFin (J)) z Ref y))$
29	28	ralimdva	$⊢ J \in Comp \to (\forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap Fin) z Ref y) \to \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap LocFin (J)) z Ref y))$
30	7 29	mpd	$⊢ J \in Comp \to \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap LocFin (J)) z Ref y)$
31		ispcmp	$⊢ J \in Paracomp \leftrightarrow J \in CovHasRef LocFin (J)$
32	4	iscref	$⊢ J \in CovHasRef LocFin (J) \leftrightarrow (J \in Top \land \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap LocFin (J)) z Ref y))$
33	31 32	bitri	$⊢ J \in Paracomp \leftrightarrow (J \in Top \land \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 J \cap LocFin (J)) z Ref y))$
34	1 30 33	sylanbrc	$⊢ J \in Comp \to J \in Paracomp$

Metamath Proof Explorer

Theorem cmppcmp

Proof