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	No typesetting found for |- S = ( Spec ` R ) with typecode |-
	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	Could not format S = ( Spec ` R ) : No typesetting found for |- S = ( Spec ` R ) with typecode |-
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	Could not format ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
5		sseq2	$$⊢j=l\to \left(k\subseteq j\leftrightarrow k\subseteq l\right)$$
6	5	cbvrabv	Could not format { j e. ( PrmIdeal ` R ) | k C_ j } = { l e. ( PrmIdeal ` R ) | k C_ l } : No typesetting found for |- { j e. ( PrmIdeal ` R ) | k C_ j } = { l e. ( PrmIdeal ` R ) | k C_ l } with typecode |-
7	4 6	eqtrdi	Could not format ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { l e. ( PrmIdeal ` R ) | k C_ l } ) : No typesetting found for |- ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { l e. ( PrmIdeal ` R ) | k C_ l } ) with typecode |-
8	7	cbvmptv	Could not format ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( k e. ( LIdeal ` R ) |-> { l e. ( PrmIdeal ` R ) | k C_ l } ) : No typesetting found for |- ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( k e. ( LIdeal ` R ) |-> { l e. ( PrmIdeal ` R ) | k C_ l } ) with typecode |-
9	1 2 8	zarcmplem	$$⊢R\in \mathrm{CRing}\to J\in \mathrm{Comp}$$