Metamath Proof Explorer

Theorem cmpfiiin

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
Hypotheses cmpfiiin.x ⊢ X = ⋃ J
cmpfiiin.j ⊢ φ → J ∈ Comp
cmpfiiin.s ⊢ φ ∧ k ∈ I → S ∈ Clsd ⁡ J
cmpfiiin.z ⊢ φ ∧ l ⊆ I ∧ l ∈ Fin → X ∩ ⋂ k ∈ l S ≠ ∅
Assertion cmpfiiin ⊢ φ → X ∩ ⋂ k ∈ I S ≠ ∅

Proof

Step Hyp Ref Expression
1 cmpfiiin.x ⊢ X = ⋃ J
2 cmpfiiin.j ⊢ φ → J ∈ Comp
3 cmpfiiin.s ⊢ φ ∧ k ∈ I → S ∈ Clsd ⁡ J
4 cmpfiiin.z ⊢ φ ∧ l ⊆ I ∧ l ∈ Fin → X ∩ ⋂ k ∈ l S ≠ ∅
5 cmptop ⊢ J ∈ Comp → J ∈ Top
6 2 5 syl ⊢ φ → J ∈ Top
7 1 topcld ⊢ J ∈ Top → X ∈ Clsd ⁡ J
8 6 7 syl ⊢ φ → X ∈ Clsd ⁡ J
9 1 cldss ⊢ S ∈ Clsd ⁡ J → S ⊆ X
10 3 9 syl ⊢ φ ∧ k ∈ I → S ⊆ X
11 10 ralrimiva ⊢ φ → ∀ k ∈ I S ⊆ X
12 riinint ⊢ X ∈ Clsd ⁡ J ∧ ∀ k ∈ I S ⊆ X → X ∩ ⋂ k ∈ I S = ⋂ X ∪ ran ⁡ k ∈ I ⟼ S
13 8 11 12 syl2anc ⊢ φ → X ∩ ⋂ k ∈ I S = ⋂ X ∪ ran ⁡ k ∈ I ⟼ S
14 8 snssd ⊢ φ → X ⊆ Clsd ⁡ J
15 3 fmpttd ⊢ φ → k ∈ I ⟼ S : I ⟶ Clsd ⁡ J
16 15 frnd ⊢ φ → ran ⁡ k ∈ I ⟼ S ⊆ Clsd ⁡ J
17 14 16 unssd ⊢ φ → X ∪ ran ⁡ k ∈ I ⟼ S ⊆ Clsd ⁡ J
18 elin ⊢ l ∈ 𝒫 I ∩ Fin ↔ l ∈ 𝒫 I ∧ l ∈ Fin
19 elpwi ⊢ l ∈ 𝒫 I → l ⊆ I
20 19 anim1i ⊢ l ∈ 𝒫 I ∧ l ∈ Fin → l ⊆ I ∧ l ∈ Fin
21 18 20 sylbi ⊢ l ∈ 𝒫 I ∩ Fin → l ⊆ I ∧ l ∈ Fin
22 nesym ⊢ X ∩ ⋂ k ∈ l S ≠ ∅ ↔ ¬ ∅ = X ∩ ⋂ k ∈ l S
23 4 22 sylib ⊢ φ ∧ l ⊆ I ∧ l ∈ Fin → ¬ ∅ = X ∩ ⋂ k ∈ l S
24 21 23 sylan2 ⊢ φ ∧ l ∈ 𝒫 I ∩ Fin → ¬ ∅ = X ∩ ⋂ k ∈ l S
25 24 nrexdv ⊢ φ → ¬ ∃ l ∈ 𝒫 I ∩ Fin ∅ = X ∩ ⋂ k ∈ l S
26 elrfirn2 ⊢ X ∈ Clsd ⁡ J ∧ ∀ k ∈ I S ⊆ X → ∅ ∈ fi ⁡ X ∪ ran ⁡ k ∈ I ⟼ S ↔ ∃ l ∈ 𝒫 I ∩ Fin ∅ = X ∩ ⋂ k ∈ l S
27 8 11 26 syl2anc ⊢ φ → ∅ ∈ fi ⁡ X ∪ ran ⁡ k ∈ I ⟼ S ↔ ∃ l ∈ 𝒫 I ∩ Fin ∅ = X ∩ ⋂ k ∈ l S
28 25 27 mtbird ⊢ φ → ¬ ∅ ∈ fi ⁡ X ∪ ran ⁡ k ∈ I ⟼ S
29 cmpfii ⊢ J ∈ Comp ∧ X ∪ ran ⁡ k ∈ I ⟼ S ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ X ∪ ran ⁡ k ∈ I ⟼ S → ⋂ X ∪ ran ⁡ k ∈ I ⟼ S ≠ ∅
30 2 17 28 29 syl3anc ⊢ φ → ⋂ X ∪ ran ⁡ k ∈ I ⟼ S ≠ ∅
31 13 30 eqnetrd ⊢ φ → X ∩ ⋂ k ∈ I S ≠ ∅