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	⊢ ( 𝜑 → ( 𝑋 ∩ ∩ 𝑘 ∈ 𝐼 𝑆 ) ≠ ∅ )