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 ‘ 𝑋 ) ) → 𝑋 ≠ ∅ )