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 No typesetting found for |- S = ( Spec ` R ) with typecode |-
zartop.2 ⊢ J = TopOpen ⁡ S
Assertion zartop ⊢ R ∈ CRing → J ∈ Top

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 = TopOpen ⁡ S
3 eqid Could not format ( PrmIdeal ` R ) = ( PrmIdeal ` R ) : No typesetting found for |- ( PrmIdeal ` R ) = ( PrmIdeal ` R ) with typecode |-
4 sseq1 ⊢ i = k → i ⊆ j ↔ k ⊆ j
5 4 rabbidv Could not format ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
6 5 cbvmptv Could not format ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
7 1 2 3 6 zartopn Could not format ( R e. CRing -> ( J e. ( TopOn ` ( PrmIdeal ` R ) ) /\ ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( Clsd ` J ) ) ) : No typesetting found for |- ( R e. CRing -> ( J e. ( TopOn ` ( PrmIdeal ` R ) ) /\ ran ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) = ( Clsd ` J ) ) ) with typecode |-
8 7 simpld Could not format ( R e. CRing -> J e. ( TopOn ` ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( R e. CRing -> J e. ( TopOn ` ( PrmIdeal ` R ) ) ) with typecode |-
9 topontop Could not format ( J e. ( TopOn ` ( PrmIdeal ` R ) ) -> J e. Top ) : No typesetting found for |- ( J e. ( TopOn ` ( PrmIdeal ` R ) ) -> J e. Top ) with typecode |-
10 8 9 syl ⊢ R ∈ CRing → J ∈ Top