Metamath Proof Explorer

Theorem cmppcmp

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

Ref Expression
Assertion cmppcmp ( 𝐽 ∈ Comp → 𝐽 ∈ Paracomp )

Proof

Step Hyp Ref Expression
1 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
2 cmpcref ⊢ Comp = CovHasRef Fin
3 2 eleq2i ⊢ ( 𝐽 ∈ Comp ↔ 𝐽 ∈ CovHasRef Fin )
4 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
5 4 iscref ⊢ ( 𝐽 ∈ CovHasRef Fin ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) 𝑧 Ref 𝑦 ) ) )
6 3 5 bitri ⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) 𝑧 Ref 𝑦 ) ) )
7 6 simprbi ⊢ ( 𝐽 ∈ Comp → ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) 𝑧 Ref 𝑦 ) )
8 simprl ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) )
9 elin ⊢ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ↔ ( 𝑧 ∈ 𝒫 𝐽 ∧ 𝑧 ∈ Fin ) )
10 8 9 sylib ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → ( 𝑧 ∈ 𝒫 𝐽 ∧ 𝑧 ∈ Fin ) )
11 10 simpld ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → 𝑧 ∈ 𝒫 𝐽 )
12 1 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → 𝐽 ∈ Top )
13 10 simprd ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → 𝑧 ∈ Fin )
14 simplr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → ∪ 𝐽 = ∪ 𝑦 )
15 simprr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → 𝑧 Ref 𝑦 )
16 eqid ⊢ ∪ 𝑧 = ∪ 𝑧
17 eqid ⊢ ∪ 𝑦 = ∪ 𝑦
18 16 17 refbas ⊢ ( 𝑧 Ref 𝑦 → ∪ 𝑦 = ∪ 𝑧 )
19 15 18 syl ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → ∪ 𝑦 = ∪ 𝑧 )
20 14 19 eqtrd ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → ∪ 𝐽 = ∪ 𝑧 )
21 4 16 finlocfin ⊢ ( ( 𝐽 ∈ Top ∧ 𝑧 ∈ Fin ∧ ∪ 𝐽 = ∪ 𝑧 ) → 𝑧 ∈ ( LocFin ‘ 𝐽 ) )
22 12 13 20 21 syl3anc ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → 𝑧 ∈ ( LocFin ‘ 𝐽 ) )
23 11 22 elind ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) )
24 23 15 jca ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) ) → ( 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) ∧ 𝑧 Ref 𝑦 ) )
25 24 ex ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) → ( ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ∧ 𝑧 Ref 𝑦 ) → ( 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) ∧ 𝑧 Ref 𝑦 ) ) )
26 25 reximdv2 ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) ∧ ∪ 𝐽 = ∪ 𝑦 ) → ( ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) 𝑧 Ref 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑧 Ref 𝑦 ) )
27 26 ex ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) → ( ∪ 𝐽 = ∪ 𝑦 → ( ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) 𝑧 Ref 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑧 Ref 𝑦 ) ) )
28 27 a2d ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽 ) → ( ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) 𝑧 Ref 𝑦 ) → ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑧 Ref 𝑦 ) ) )
29 28 ralimdva ⊢ ( 𝐽 ∈ Comp → ( ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) 𝑧 Ref 𝑦 ) → ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑧 Ref 𝑦 ) ) )
30 7 29 mpd ⊢ ( 𝐽 ∈ Comp → ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑧 Ref 𝑦 ) )
31 ispcmp ⊢ ( 𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef ( LocFin ‘ 𝐽 ) )
32 4 iscref ⊢ ( 𝐽 ∈ CovHasRef ( LocFin ‘ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑧 Ref 𝑦 ) ) )
33 31 32 bitri ⊢ ( 𝐽 ∈ Paracomp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ ( LocFin ‘ 𝐽 ) ) 𝑧 Ref 𝑦 ) ) )
34 1 30 33 sylanbrc ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Paracomp )