Theorem zarcmp

Description: The Zariski topology is compact. Proposition 1.1.10(ii) of EGA, p. 82. (Contributed by Thierry Arnoux, 2-Jul-2024)

	Ref	Expression
Hypotheses	zartop.1	$$⊢S=\mathrm{Spec}\left(R\right)$$
	zartop.2	$$⊢J=\mathrm{TopOpen}\left(S\right)$$
Assertion	zarcmp	$$⊢R\in \mathrm{CRing}\to J\in \mathrm{Comp}$$

Proof

Step	Hyp	Ref	Expression
1		zartop.1	$$⊢S=\mathrm{Spec}\left(R\right)$$
2		zartop.2	$$⊢J=\mathrm{TopOpen}\left(S\right)$$
3		sseq1	$$⊢i=k\to \left(i\subseteq j\leftrightarrow k\subseteq j\right)$$
4	3	rabbidv	$$⊢i=k\to \left\{j\in \mathrm{PrmIdeal}\left(R\right)|i\subseteq j\right\}=\left\{j\in \mathrm{PrmIdeal}\left(R\right)|k\subseteq j\right\}$$
5		sseq2	$$⊢j=l\to \left(k\subseteq j\leftrightarrow k\subseteq l\right)$$
6	5	cbvrabv	$$⊢\left\{j\in \mathrm{PrmIdeal}\left(R\right)|k\subseteq j\right\}=\left\{l\in \mathrm{PrmIdeal}\left(R\right)|k\subseteq l\right\}$$
7	4 6	eqtrdi	$$⊢i=k\to \left\{j\in \mathrm{PrmIdeal}\left(R\right)|i\subseteq j\right\}=\left\{l\in \mathrm{PrmIdeal}\left(R\right)|k\subseteq l\right\}$$
8	7	cbvmptv	$$⊢\left(i\in \mathrm{LIdeal}\left(R\right)⟼\left\{j\in \mathrm{PrmIdeal}\left(R\right)|i\subseteq j\right\}\right)=\left(k\in \mathrm{LIdeal}\left(R\right)⟼\left\{l\in \mathrm{PrmIdeal}\left(R\right)|k\subseteq l\right\}\right)$$
9	1 2 8	zarcmplem	$$⊢R\in \mathrm{CRing}\to J\in \mathrm{Comp}$$