Metamath Proof Explorer

Theorem rspectset

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

Ref Expression
Hypotheses rspecbas.1 ⊢ S = Spec ⁡ R
rspectset.1 ⊢ I = LIdeal ⁡ R
rspectset.2 ⊢ J = ran ⁡ i ∈ I ⟼ j ∈ I | ¬ i ⊆ j
Assertion rspectset ⊢ R ∈ Ring → J = TopSet ⁡ S

Proof

Step Hyp Ref Expression
1 rspecbas.1 ⊢ S = Spec ⁡ R
2 rspectset.1 ⊢ I = LIdeal ⁡ R
3 rspectset.2 ⊢ J = ran ⁡ i ∈ I ⟼ j ∈ I | ¬ i ⊆ j
4 fvex ⊢ PrmIdeal ⁡ R ∈ V
5 eqid ⊢ IDLsrg ⁡ R ↾ 𝑠 PrmIdeal ⁡ R = IDLsrg ⁡ R ↾ 𝑠 PrmIdeal ⁡ R
6 eqid ⊢ TopSet ⁡ IDLsrg ⁡ R = TopSet ⁡ IDLsrg ⁡ R
7 5 6 resstset ⊢ PrmIdeal ⁡ R ∈ V → TopSet ⁡ IDLsrg ⁡ R = TopSet ⁡ IDLsrg ⁡ R ↾ 𝑠 PrmIdeal ⁡ R
8 4 7 ax-mp ⊢ TopSet ⁡ IDLsrg ⁡ R = TopSet ⁡ IDLsrg ⁡ R ↾ 𝑠 PrmIdeal ⁡ R
9 eqid ⊢ IDLsrg ⁡ R = IDLsrg ⁡ R
10 9 2 3 idlsrgtset ⊢ R ∈ Ring → J = TopSet ⁡ IDLsrg ⁡ R
11 rspecval ⊢ R ∈ Ring → Spec ⁡ R = IDLsrg ⁡ R ↾ 𝑠 PrmIdeal ⁡ R
12 1 11 eqtrid ⊢ R ∈ Ring → S = IDLsrg ⁡ R ↾ 𝑠 PrmIdeal ⁡ R
13 12 fveq2d ⊢ R ∈ Ring → TopSet ⁡ S = TopSet ⁡ IDLsrg ⁡ R ↾ 𝑠 PrmIdeal ⁡ R
14 8 10 13 3eqtr4a ⊢ R ∈ Ring → J = TopSet ⁡ S