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	No typesetting found for |- S = ( Spec ` R ) with typecode |-
	zartop.2	$$⊢J=\mathrm{TopOpen}\left(S\right)$$
	zartop.3	No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
Assertion	zartopon	$$⊢R\in \mathrm{CRing}\to J\in \mathrm{TopOn}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		zartop.1	Could not format S = ( Spec ` R ) : No typesetting found for |- S = ( Spec ` R ) with typecode |-
2		zartop.2	$$⊢J=\mathrm{TopOpen}\left(S\right)$$
3		zartop.3	Could not format P = ( PrmIdeal ` R ) : No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
4		sseq1	$$⊢i=k\to \left(i\subseteq j\leftrightarrow k\subseteq j\right)$$
5	4	rabbidv	$$⊢i=k\to \left\{j\in P|i\subseteq j\right\}=\left\{j\in P|k\subseteq j\right\}$$
6	5	cbvmptv	$$⊢\left(i\in \mathrm{LIdeal}\left(R\right)⟼\left\{j\in P|i\subseteq j\right\}\right)=\left(k\in \mathrm{LIdeal}\left(R\right)⟼\left\{j\in P|k\subseteq j\right\}\right)$$
7	1 2 3 6	zartopn	$$⊢R\in \mathrm{CRing}\to \left(J\in \mathrm{TopOn}\left(P\right)\wedge \mathrm{ran}\left(i\in \mathrm{LIdeal}\left(R\right)⟼\left\{j\in P|i\subseteq j\right\}\right)=\mathrm{Clsd}\left(J\right)\right)$$
8	7	simpld	$$⊢R\in \mathrm{CRing}\to J\in \mathrm{TopOn}\left(P\right)$$