Metamath Proof Explorer

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 ⊢ S = Spec ⁡ R
zartop.2 ⊢ J = TopOpen ⁡ S
Assertion zartop ⊢ R ∈ CRing → J ∈ Top

Proof

Step Hyp Ref Expression
1 zartop.1 ⊢ S = Spec ⁡ R
2 zartop.2 ⊢ J = TopOpen ⁡ S
3 eqid ⊢ PrmIdeal ⁡ R = PrmIdeal ⁡ R
4 sseq1 ⊢ i = k → i ⊆ j ↔ k ⊆ j
5 4 rabbidv ⊢ i = k → j ∈ PrmIdeal ⁡ R | i ⊆ j = j ∈ PrmIdeal ⁡ R | k ⊆ j
6 5 cbvmptv ⊢ i ∈ LIdeal ⁡ R ⟼ j ∈ PrmIdeal ⁡ R | i ⊆ j = k ∈ LIdeal ⁡ R ⟼ j ∈ PrmIdeal ⁡ R | k ⊆ j
7 1 2 3 6 zartopn ⊢ R ∈ CRing → J ∈ TopOn ⁡ PrmIdeal ⁡ R ∧ ran ⁡ i ∈ LIdeal ⁡ R ⟼ j ∈ PrmIdeal ⁡ R | i ⊆ j = Clsd ⁡ J
8 7 simpld ⊢ R ∈ CRing → J ∈ TopOn ⁡ PrmIdeal ⁡ R
9 topontop ⊢ J ∈ TopOn ⁡ PrmIdeal ⁡ R → J ∈ Top
10 8 9 syl ⊢ R ∈ CRing → J ∈ Top