pcmplfin

Description: Given a paracompact topology J and an open cover U , there exists an open refinement v that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020)

		Ref	Expression
	Hypothesis	pcmplfin.x	$⊢ X = ⋃ J$
	Assertion	pcmplfin	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to \exists v \in 𝒫 J (v \in LocFin (J) \land v Ref U)$

Proof

Step	Hyp	Ref	Expression
1		pcmplfin.x	$⊢ X = ⋃ J$
2		ssexg	$⊢ (U \subseteq J \land J \in Paracomp) \to U \in V$
3	2	ancoms	$⊢ (J \in Paracomp \land U \subseteq J) \to U \in V$
4	3	3adant3	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to U \in V$
5		simp2	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to U \subseteq J$
6	4 5	elpwd	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to U \in 𝒫 J$
7		ispcmp	$⊢ J \in Paracomp \leftrightarrow J \in CovHasRef LocFin (J)$
8	1	iscref	$⊢ J \in CovHasRef LocFin (J) \leftrightarrow (J \in Top \land \forall u \in 𝒫 J (X = ⋃ u \to \exists v \in (𝒫 J \cap LocFin (J)) v Ref u))$
9	7 8	bitri	$⊢ J \in Paracomp \leftrightarrow (J \in Top \land \forall u \in 𝒫 J (X = ⋃ u \to \exists v \in (𝒫 J \cap LocFin (J)) v Ref u))$
10	9	simprbi	$⊢ J \in Paracomp \to \forall u \in 𝒫 J (X = ⋃ u \to \exists v \in (𝒫 J \cap LocFin (J)) v Ref u)$
11	10	3ad2ant1	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to \forall u \in 𝒫 J (X = ⋃ u \to \exists v \in (𝒫 J \cap LocFin (J)) v Ref u)$
12		simp3	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to X = ⋃ U$
13		unieq	$⊢ u = U \to ⋃ u = ⋃ U$
14	13	eqeq2d	$⊢ u = U \to (X = ⋃ u \leftrightarrow X = ⋃ U)$
15		breq2	$⊢ u = U \to (v Ref u \leftrightarrow v Ref U)$
16	15	rexbidv	$⊢ u = U \to (\exists v \in (𝒫 J \cap LocFin (J)) v Ref u \leftrightarrow \exists v \in (𝒫 J \cap LocFin (J)) v Ref U)$
17	14 16	imbi12d	$⊢ u = U \to ((X = ⋃ u \to \exists v \in (𝒫 J \cap LocFin (J)) v Ref u) \leftrightarrow (X = ⋃ U \to \exists v \in (𝒫 J \cap LocFin (J)) v Ref U))$
18	17	rspcv	$⊢ U \in 𝒫 J \to (\forall u \in 𝒫 J (X = ⋃ u \to \exists v \in (𝒫 J \cap LocFin (J)) v Ref u) \to (X = ⋃ U \to \exists v \in (𝒫 J \cap LocFin (J)) v Ref U))$
19	6 11 12 18	syl3c	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to \exists v \in (𝒫 J \cap LocFin (J)) v Ref U$
20		rexin	$⊢ \exists v \in (𝒫 J \cap LocFin (J)) v Ref U \leftrightarrow \exists v \in 𝒫 J (v \in LocFin (J) \land v Ref U)$
21	19 20	sylib	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to \exists v \in 𝒫 J (v \in LocFin (J) \land v Ref U)$

Metamath Proof Explorer

Theorem pcmplfin

Proof