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

Proof

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