Theorem rspectset

Description: Topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024)

	Ref	Expression
Hypotheses	rspecbas.1	|- S = ( Spec ` R )
	rspectset.1	|- I = ( LIdeal ` R )
	rspectset.2	|- J = ran ( i e. I |-> { j e. I | -. i C_ j } )
Assertion	rspectset	|- ( R e. Ring -> J = ( TopSet ` S ) )

Proof

Step	Hyp	Ref	Expression
1		rspecbas.1	|- S = ( Spec ` R )
2		rspectset.1	|- I = ( LIdeal ` R )
3		rspectset.2	|- J = ran ( i e. I |-> { j e. I | -. i C_ j } )
4		fvex	|- ( PrmIdeal ` R ) e. _V
5		eqid	|- ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) )
6		eqid	|- ( TopSet ` ( IDLsrg ` R ) ) = ( TopSet ` ( IDLsrg ` R ) )
7	5 6	resstset	|- ( ( PrmIdeal ` R ) e. _V -> ( TopSet ` ( IDLsrg ` R ) ) = ( TopSet ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) )
8	4 7	ax-mp	|- ( TopSet ` ( IDLsrg ` R ) ) = ( TopSet ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) )
9		eqid	|- ( IDLsrg ` R ) = ( IDLsrg ` R )
10	9 2 3	idlsrgtset	|- ( R e. Ring -> J = ( TopSet ` ( IDLsrg ` R ) ) )
11		rspecval	|- ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) )
12	1 11	eqtrid	|- ( R e. Ring -> S = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) )
13	12	fveq2d	|- ( R e. Ring -> ( TopSet ` S ) = ( TopSet ` ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) )
14	8 10 13	3eqtr4a	|- ( R e. Ring -> J = ( TopSet ` S ) )