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	⊢ 𝑋 = ∪ 𝐽
Assertion	pcmplfinf	⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pcmplfin.x	⊢ 𝑋 = ∪ 𝐽
2		simpll2	⊢ ( ( ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) ∧ 𝑣 ∈ 𝒫 𝐽 ) ∧ ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) ) → 𝑈 ⊆ 𝐽 )
3		simpll3	⊢ ( ( ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) ∧ 𝑣 ∈ 𝒫 𝐽 ) ∧ ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) ) → 𝑋 = ∪ 𝑈 )
4		elpwi	⊢ ( 𝑣 ∈ 𝒫 𝐽 → 𝑣 ⊆ 𝐽 )
5	4	ad2antlr	⊢ ( ( ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) ∧ 𝑣 ∈ 𝒫 𝐽 ) ∧ ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) ) → 𝑣 ⊆ 𝐽 )
6		simprr	⊢ ( ( ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) ∧ 𝑣 ∈ 𝒫 𝐽 ) ∧ ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) ) → 𝑣 Ref 𝑈 )
7		simprl	⊢ ( ( ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) ∧ 𝑣 ∈ 𝒫 𝐽 ) ∧ ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) ) → 𝑣 ∈ ( LocFin ‘ 𝐽 ) )
8	1 2 3 5 6 7	locfinref	⊢ ( ( ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) ∧ 𝑣 ∈ 𝒫 𝐽 ) ∧ ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )
9	1	pcmplfin	⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑣 ∈ 𝒫 𝐽 ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) )
10	8 9	r19.29a	⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑓 ( 𝑓 : 𝑈 ⟶ 𝐽 ∧ ran 𝑓 Ref 𝑈 ∧ ran 𝑓 ∈ ( LocFin ‘ 𝐽 ) ) )