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	⊢ 𝑆 = ( Spec ‘ 𝑅 )
	zartop.2	⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
	zartop.3	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
Assertion	zartopon	⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ ( TopOn ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		zartop.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
2		zartop.2	⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
3		zartop.3	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
4		sseq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑗 ) )
5	4	rabbidv	⊢ ( 𝑖 = 𝑘 → { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ 𝑃 ∣ 𝑘 ⊆ 𝑗 } )
6	5	cbvmptv	⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) = ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ 𝑘 ⊆ 𝑗 } )
7	1 2 3 6	zartopn	⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ ( TopOn ‘ 𝑃 ) ∧ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) = ( Clsd ‘ 𝐽 ) ) )
8	7	simpld	⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ ( TopOn ‘ 𝑃 ) )