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 = ( Spec ` R )
	zartop.2	|- J = ( TopOpen ` S )
Assertion	zarcmp	|- ( R e. CRing -> J e. Comp )

Proof

Step	Hyp	Ref	Expression
1		zartop.1	|- S = ( Spec ` R )
2		zartop.2	|- J = ( TopOpen ` S )
3		sseq1	|- ( i = k -> ( i C_ j <-> k C_ j ) )
4	3	rabbidv	|- ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | k C_ j } )
5		sseq2	|- ( j = l -> ( k C_ j <-> k C_ l ) )
6	5	cbvrabv	|- { j e. ( PrmIdeal ` R ) | k C_ j } = { l e. ( PrmIdeal ` R ) | k C_ l }
7	4 6	eqtrdi	|- ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { l e. ( PrmIdeal ` R ) | k C_ l } )
8	7	cbvmptv	|- ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( k e. ( LIdeal ` R ) |-> { l e. ( PrmIdeal ` R ) | k C_ l } )
9	1 2 8	zarcmplem	|- ( R e. CRing -> J e. Comp )