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∈lS≠∅
Assertion cmpfiiin ⊢φ→X∩⋂k∈IS≠∅

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∈lS≠∅
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∈IS⊆X
12 riinint ⊢X∈Clsd⁡J∧∀k∈IS⊆X→X∩⋂k∈IS=⋂X∪ran⁡k∈I⟼S
13 8 11 12 syl2anc ⊢φ→X∩⋂k∈IS=⋂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∈lS≠∅↔¬∅=X∩⋂k∈lS
23 4 22 sylib ⊢φ∧l⊆I∧l∈Fin→¬∅=X∩⋂k∈lS
24 21 23 sylan2 ⊢φ∧l∈𝒫I∩Fin→¬∅=X∩⋂k∈lS
25 24 nrexdv ⊢φ→¬∃l∈𝒫I∩Fin∅=X∩⋂k∈lS
26 elrfirn2 ⊢X∈Clsd⁡J∧∀k∈IS⊆X→∅∈fi⁡X∪ran⁡k∈I⟼S↔∃l∈𝒫I∩Fin∅=X∩⋂k∈lS
27 8 11 26 syl2anc ⊢φ→∅∈fi⁡X∪ran⁡k∈I⟼S↔∃l∈𝒫I∩Fin∅=X∩⋂k∈lS
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∈IS≠∅