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