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 ≠ ∅