This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
cmpfiiin.j ⊢ ( 𝜑 → 𝐽 ∈ Comp )
cmpfiiin.s ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
cmpfiiin.z ⊢ ( ( 𝜑 ∧ ( 𝑙 ⊆ 𝐼 ∧ 𝑙 ∈ Fin ) ) → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆 ) ≠ ∅ )
Assertion cmpfiiin ( 𝜑 → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 cmpfiiin.x ⊢ 𝑋 = ∪ 𝐽
2 cmpfiiin.j ⊢ ( 𝜑 → 𝐽 ∈ Comp )
3 cmpfiiin.s ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
4 cmpfiiin.z ⊢ ( ( 𝜑 ∧ ( 𝑙 ⊆ 𝐼 ∧ 𝑙 ∈ Fin ) ) → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆 ) ≠ ∅ )
5 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
6 2 5 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
7 1 topcld ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
8 6 7 syl ⊢ ( 𝜑 → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
9 1 cldss ⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝑆 ⊆ 𝑋 )
10 3 9 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑆 ⊆ 𝑋 )
11 10 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 )
12 riinint ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆 ) = ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) )
13 8 11 12 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆 ) = ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) )
14 8 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ ( Clsd ‘ 𝐽 ) )
15 3 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) : 𝐼 ⟶ ( Clsd ‘ 𝐽 ) )
16 15 frnd ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ⊆ ( Clsd ‘ 𝐽 ) )
17 14 16 unssd ⊢ ( 𝜑 → ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) ⊆ ( Clsd ‘ 𝐽 ) )
18 elin ⊢ ( 𝑙 ∈ ( 𝒫 𝐼 ∩ Fin ) ↔ ( 𝑙 ∈ 𝒫 𝐼 ∧ 𝑙 ∈ Fin ) )
19 elpwi ⊢ ( 𝑙 ∈ 𝒫 𝐼 → 𝑙 ⊆ 𝐼 )
20 19 anim1i ⊢ ( ( 𝑙 ∈ 𝒫 𝐼 ∧ 𝑙 ∈ Fin ) → ( 𝑙 ⊆ 𝐼 ∧ 𝑙 ∈ Fin ) )
21 18 20 sylbi ⊢ ( 𝑙 ∈ ( 𝒫 𝐼 ∩ Fin ) → ( 𝑙 ⊆ 𝐼 ∧ 𝑙 ∈ Fin ) )
22 nesym ⊢ ( ( 𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆 ) ≠ ∅ ↔ ¬ ∅ = ( 𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆 ) )
23 4 22 sylib ⊢ ( ( 𝜑 ∧ ( 𝑙 ⊆ 𝐼 ∧ 𝑙 ∈ Fin ) ) → ¬ ∅ = ( 𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆 ) )
24 21 23 sylan2 ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → ¬ ∅ = ( 𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆 ) )
25 24 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑙 ∈ ( 𝒫 𝐼 ∩ Fin ) ∅ = ( 𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆 ) )
26 elrfirn2 ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ∀ 𝑘 ∈ 𝐼 𝑆 ⊆ 𝑋 ) → ( ∅ ∈ ( fi ‘ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) ) ↔ ∃ 𝑙 ∈ ( 𝒫 𝐼 ∩ Fin ) ∅ = ( 𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆 ) ) )
27 8 11 26 syl2anc ⊢ ( 𝜑 → ( ∅ ∈ ( fi ‘ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) ) ↔ ∃ 𝑙 ∈ ( 𝒫 𝐼 ∩ Fin ) ∅ = ( 𝑋 ∩ ∩ 𝑘 ∈ 𝑙 𝑆 ) ) )
28 25 27 mtbird ⊢ ( 𝜑 → ¬ ∅ ∈ ( fi ‘ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) ) )
29 cmpfii ⊢ ( ( 𝐽 ∈ Comp ∧ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) ⊆ ( Clsd ‘ 𝐽 ) ∧ ¬ ∅ ∈ ( fi ‘ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) ) ) → ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) ≠ ∅ )
30 2 17 28 29 syl3anc ⊢ ( 𝜑 → ∩ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐼 ↦ 𝑆 ) ) ≠ ∅ )
31 13 30 eqnetrd ⊢ ( 𝜑 → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆 ) ≠ ∅ )