Metamath Proof Explorer

Theorem pcmplfinf

Description: Given a paracompact topology J and an open cover U , there exists an open refinement ran f that is locally finite, using the same index as the original cover U . (Contributed by Thierry Arnoux, 31-Jan-2020)

		Ref	Expression
	Hypothesis	pcmplfin.x	$⊢ X = ⋃ J$
	Assertion	pcmplfinf	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J))$

Proof

Step	Hyp	Ref	Expression
1		pcmplfin.x	$⊢ X = ⋃ J$
2		simpll2	$⊢ (((J \in Paracomp \land U \subseteq J \land X = ⋃ U) \land v \in 𝒫 J) \land (v \in LocFin (J) \land v Ref U)) \to U \subseteq J$
3		simpll3	$⊢ (((J \in Paracomp \land U \subseteq J \land X = ⋃ U) \land v \in 𝒫 J) \land (v \in LocFin (J) \land v Ref U)) \to X = ⋃ U$
4		elpwi	$⊢ v \in 𝒫 J \to v \subseteq J$
5	4	ad2antlr	$⊢ (((J \in Paracomp \land U \subseteq J \land X = ⋃ U) \land v \in 𝒫 J) \land (v \in LocFin (J) \land v Ref U)) \to v \subseteq J$
6		simprr	$⊢ (((J \in Paracomp \land U \subseteq J \land X = ⋃ U) \land v \in 𝒫 J) \land (v \in LocFin (J) \land v Ref U)) \to v Ref U$
7		simprl	$⊢ (((J \in Paracomp \land U \subseteq J \land X = ⋃ U) \land v \in 𝒫 J) \land (v \in LocFin (J) \land v Ref U)) \to v \in LocFin (J)$
8	1 2 3 5 6 7	locfinref	$⊢ (((J \in Paracomp \land U \subseteq J \land X = ⋃ U) \land v \in 𝒫 J) \land (v \in LocFin (J) \land v Ref U)) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J))$
9	1	pcmplfin	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to \exists v \in 𝒫 J (v \in LocFin (J) \land v Ref U)$
10	8 9	r19.29a	$⊢ (J \in Paracomp \land U \subseteq J \land X = ⋃ U) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J))$