Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ∪ 𝐽
Assertion pcmplfin ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑣 ∈ 𝒫 𝐽 ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) )

Proof

Step Hyp Ref Expression
1 pcmplfin.x ⊢ 𝑋 = ∪ 𝐽
2 ssexg ⊢ ( ( 𝑈 ⊆ 𝐽 ∧ 𝐽 ∈ Paracomp ) → 𝑈 ∈ V )
3 2 ancoms ⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ) → 𝑈 ∈ V )
4 3 3adant3 ⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → 𝑈 ∈ V )
5 simp2 ⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → 𝑈 ⊆ 𝐽 )
6 4 5 elpwd ⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → 𝑈 ∈ 𝒫 𝐽 )
7 ispcmp ⊢ ( 𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef ( LocFin ‘ 𝐽 ) )
8 1 iscref ⊢ ( 𝐽 ∈ CovHasRef ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑢 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑢 ) ) )
9 7 8 bitri ⊢ ( 𝐽 ∈ Paracomp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑢 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑢 ) ) )
10 9 simprbi ⊢ ( 𝐽 ∈ Paracomp → ∀ 𝑢 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑢 ) )
11 10 3ad2ant1 ⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∀ 𝑢 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑢 ) )
12 simp3 ⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → 𝑋 = ∪ 𝑈 )
13 unieq ⊢ ( 𝑢 = 𝑈 → ∪ 𝑢 = ∪ 𝑈 )
14 13 eqeq2d ⊢ ( 𝑢 = 𝑈 → ( 𝑋 = ∪ 𝑢 ↔ 𝑋 = ∪ 𝑈 ) )
15 breq2 ⊢ ( 𝑢 = 𝑈 → ( 𝑣 Ref 𝑢 ↔ 𝑣 Ref 𝑈 ) )
16 15 rexbidv ⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑢 ↔ ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑈 ) )
17 14 16 imbi12d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑢 ) ↔ ( 𝑋 = ∪ 𝑈 → ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑈 ) ) )
18 17 rspcv ⊢ ( 𝑈 ∈ 𝒫 𝐽 → ( ∀ 𝑢 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑢 ) → ( 𝑋 = ∪ 𝑈 → ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑈 ) ) )
19 6 11 12 18 syl3c ⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑈 )
20 rexin ⊢ ( ∃ 𝑣 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑣 Ref 𝑈 ↔ ∃ 𝑣 ∈ 𝒫 𝐽 ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) )
21 19 20 sylib ⊢ ( ( 𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑣 ∈ 𝒫 𝐽 ( 𝑣 ∈ ( LocFin ‘ 𝐽 ) ∧ 𝑣 Ref 𝑈 ) )