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

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 ( ( 𝐽 ∈ Comp ∧ 𝑋 ⊆ ( Clsd ‘ 𝐽 ) ∧ ¬ ∅ ∈ ( fi ‘ 𝑋 ) ) → ∩ 𝑋 ≠ ∅ )

Proof

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