Proof of The Finite Intersection Property of a Compact Set

Throughout, compactness of $K$ means compactness of $(K,\mathcal{T}_{K})$ with the subspace topology, as in Compact Topological Space and Compact Subset (ii). We prove (i) by contradiction.

First, $K$ is nonempty. Indeed, fix $i_{0}\in I$; the set $\{i_{0}\}$ is finite (Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iii)), so the hypothesis gives $K\cap F_{i_{0}}\neq\emptyset$.

Now suppose that $K\cap\bigcap_{i\in I}F_{i}=\emptyset$, and consider the family of relative complements

$$\mathcal{U}=\{W\in\mathcal{P}(K):\ W=K\setminus F_{i}\text{ for some }i\in I\}.$$

Each member of $\mathcal{U}$ is open in $(K,\mathcal{T}_{K})$: it has the form $K\setminus F_{i}=K\cap(X\setminus F_{i})$, where $X\setminus F_{i}\in\mathcal{T}$ because $F_{i}$ is closed (Closed Subset of a Topological Space (i)), so it is open by Subspace Topology (ii). Moreover $\mathcal{U}$ covers $K$, since by our assumption every $u\in K$ lies outside some $F_{i}$. By compactness (Compact Topological Space and Compact Subset (i)) there is a finite subfamily $\mathcal{V}\subseteq\mathcal{U}$ with $K\subseteq\bigcup\mathcal{V}$, and $\mathcal{V}\neq\emptyset$ because $K\neq\emptyset$.

Each $W\in\mathcal{V}$ equals $K\setminus F_{i}$ for at least one $i\in I$, so Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (xi) provides a function $g:\mathcal{V}\to I$ with

$$W=K\setminus F_{g(W)}\qquad\text{for every }W\in\mathcal{V}.$$

Its image $J=g(\mathcal{V})$ is a nonempty finite subset of $I$ (Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (vi)). Every $u\in K$ lies in some $W\in\mathcal{V}$, and then $u\notin F_{g(W)}$ with $g(W)\in J$. Hence

$$K\cap\bigcap_{i\in J}F_{i}=\emptyset,$$

contradicting the hypothesis for this $J$. Therefore $K\cap\bigcap_{i\in I}F_{i}\neq\emptyset$.