Metamath Proof Explorer

Theorem cmpfii

Description: In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion cmpfii ⊢J∈Comp∧X⊆Clsd⁡J∧¬∅∈fi⁡X→⋂X≠∅

Proof

Step Hyp Ref Expression
1 fvex ⊢Clsd⁡J∈V
2 1 elpw2 ⊢X∈𝒫Clsd⁡J↔X⊆Clsd⁡J
3 2 biimpri ⊢X⊆Clsd⁡J→X∈𝒫Clsd⁡J
4 cmptop ⊢J∈Comp→J∈Top
5 cmpfi ⊢J∈Top→J∈Comp↔∀x∈𝒫Clsd⁡J¬∅∈fi⁡x→⋂x≠∅
6 4 5 syl ⊢J∈Comp→J∈Comp↔∀x∈𝒫Clsd⁡J¬∅∈fi⁡x→⋂x≠∅
7 6 ibi ⊢J∈Comp→∀x∈𝒫Clsd⁡J¬∅∈fi⁡x→⋂x≠∅
8 fveq2 ⊢x=X→fi⁡x=fi⁡X
9 8 eleq2d ⊢x=X→∅∈fi⁡x↔∅∈fi⁡X
10 9 notbid ⊢x=X→¬∅∈fi⁡x↔¬∅∈fi⁡X
11 inteq ⊢x=X→⋂x=⋂X
12 11 neeq1d ⊢x=X→⋂x≠∅↔⋂X≠∅
13 10 12 imbi12d ⊢x=X→¬∅∈fi⁡x→⋂x≠∅↔¬∅∈fi⁡X→⋂X≠∅
14 13 rspcva ⊢X∈𝒫Clsd⁡J∧∀x∈𝒫Clsd⁡J¬∅∈fi⁡x→⋂x≠∅→¬∅∈fi⁡X→⋂X≠∅
15 3 7 14 syl2anr ⊢J∈Comp∧X⊆Clsd⁡J→¬∅∈fi⁡X→⋂X≠∅
16 15 3impia ⊢J∈Comp∧X⊆Clsd⁡J∧¬∅∈fi⁡X→⋂X≠∅