Theorem zartop

Description: The Zariski topology is a topology. Proposition 1.1.2 of EGA p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zartop.1	|- S = ( Spec ` R )
	zartop.2	|- J = ( TopOpen ` S )
Assertion	zartop	|- ( R e. CRing -> J e. Top )

Proof

Step	Hyp	Ref	Expression
1		zartop.1	|- S = ( Spec ` R )
2		zartop.2	|- J = ( TopOpen ` S )
3		eqid	|- ( PrmIdeal ` R ) = ( PrmIdeal ` R )
4		sseq1	|- ( i = k -> ( i C_ j <-> k C_ j ) )
5	4	rabbidv	|- ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | k C_ j } )
6	5	cbvmptv	|- ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } )
7	1 2 3 6	zartopn	|- ( R e. CRing -> ( J e. ( TopOn ` ( PrmIdeal ` R ) ) /\ ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( Clsd ` J ) ) )
8	7	simpld	|- ( R e. CRing -> J e. ( TopOn ` ( PrmIdeal ` R ) ) )
9		topontop	|- ( J e. ( TopOn ` ( PrmIdeal ` R ) ) -> J e. Top )
10	8 9	syl	|- ( R e. CRing -> J e. Top )