Theorem zartopon

Description: The points of the Zariski topology are the prime ideals. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypotheses	zartop.1	|- S = ( Spec ` R )
	zartop.2	|- J = ( TopOpen ` S )
	zartop.3	|- P = ( PrmIdeal ` R )
Assertion	zartopon	|- ( R e. CRing -> J e. ( TopOn ` P ) )

Proof

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