Theorem rspectset

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

	Ref	Expression
Hypotheses	rspecbas.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
	rspectset.1	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
	rspectset.2	⊢ 𝐽 = ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } )
Assertion	rspectset	⊢ ( 𝑅 ∈ Ring → 𝐽 = ( TopSet ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		rspecbas.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
2		rspectset.1	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
3		rspectset.2	⊢ 𝐽 = ran ( 𝑖 ∈ 𝐼 ↦ { 𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗 } )
4		fvex	⊢ ( PrmIdeal ‘ 𝑅 ) ∈ V
5		eqid	⊢ ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) )
6		eqid	⊢ ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) = ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) )
7	5 6	resstset	⊢ ( ( PrmIdeal ‘ 𝑅 ) ∈ V → ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) = ( TopSet ‘ ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) ) )
8	4 7	ax-mp	⊢ ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) = ( TopSet ‘ ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) )
9		eqid	⊢ ( IDLsrg ‘ 𝑅 ) = ( IDLsrg ‘ 𝑅 )
10	9 2 3	idlsrgtset	⊢ ( 𝑅 ∈ Ring → 𝐽 = ( TopSet ‘ ( IDLsrg ‘ 𝑅 ) ) )
11		rspecval	⊢ ( 𝑅 ∈ Ring → ( Spec ‘ 𝑅 ) = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) )
12	1 11	syl5eq	⊢ ( 𝑅 ∈ Ring → 𝑆 = ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) )
13	12	fveq2d	⊢ ( 𝑅 ∈ Ring → ( TopSet ‘ 𝑆 ) = ( TopSet ‘ ( ( IDLsrg ‘ 𝑅 ) ↾s ( PrmIdeal ‘ 𝑅 ) ) ) )
14	8 10 13	3eqtr4a	⊢ ( 𝑅 ∈ Ring → 𝐽 = ( TopSet ‘ 𝑆 ) )