Metamath Proof Explorer


Theorem zarcls

Description: The open sets of the Zariski topology are the complements of the closed sets. (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
zarcls.1 No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
zarcls.2 V = i LIdeal R j P | i j
Assertion zarcls R Ring J = s 𝒫 P | P s ran V

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 zarcls.1 Could not format P = ( PrmIdeal ` R ) : No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
4 zarcls.2 V = i LIdeal R j P | i j
5 eqid LIdeal R = LIdeal R
6 eqid ran i LIdeal R j P | ¬ i j = ran i LIdeal R j P | ¬ i j
7 1 5 3 6 rspectopn R Ring ran i LIdeal R j P | ¬ i j = TopOpen S
8 2 7 eqtr4id R Ring J = ran i LIdeal R j P | ¬ i j
9 nfv s R Ring
10 nfcv _ s ran i LIdeal R j P | ¬ i j
11 nfrab1 _ s s 𝒫 P | P s ran V
12 notrab P j P | i j = j P | ¬ i j
13 12 eqeq2i s = P j P | i j s = j P | ¬ i j
14 ssrab2 j P | i j P
15 14 a1i s 𝒫 P j P | i j P
16 elpwi s 𝒫 P s P
17 ssdifsym j P | i j P s P s = P j P | i j j P | i j = P s
18 15 16 17 syl2anc s 𝒫 P s = P j P | i j j P | i j = P s
19 eqcom j P | i j = P s P s = j P | i j
20 18 19 bitrdi s 𝒫 P s = P j P | i j P s = j P | i j
21 13 20 bitr3id s 𝒫 P s = j P | ¬ i j P s = j P | i j
22 21 ad2antlr R Ring s 𝒫 P i LIdeal R s = j P | ¬ i j P s = j P | i j
23 22 rexbidva R Ring s 𝒫 P i LIdeal R s = j P | ¬ i j i LIdeal R P s = j P | i j
24 3 fvexi P V
25 24 rabex j P | i j V
26 4 25 elrnmpti P s ran V i LIdeal R P s = j P | i j
27 23 26 bitr4di R Ring s 𝒫 P i LIdeal R s = j P | ¬ i j P s ran V
28 27 pm5.32da R Ring s 𝒫 P i LIdeal R s = j P | ¬ i j s 𝒫 P P s ran V
29 ssrab2 j P | ¬ i j P
30 24 elpw2 j P | ¬ i j 𝒫 P j P | ¬ i j P
31 29 30 mpbir j P | ¬ i j 𝒫 P
32 31 rgenw i LIdeal R j P | ¬ i j 𝒫 P
33 eqid i LIdeal R j P | ¬ i j = i LIdeal R j P | ¬ i j
34 33 rnmptss i LIdeal R j P | ¬ i j 𝒫 P ran i LIdeal R j P | ¬ i j 𝒫 P
35 32 34 ax-mp ran i LIdeal R j P | ¬ i j 𝒫 P
36 35 sseli s ran i LIdeal R j P | ¬ i j s 𝒫 P
37 36 pm4.71ri s ran i LIdeal R j P | ¬ i j s 𝒫 P s ran i LIdeal R j P | ¬ i j
38 vex s V
39 33 elrnmpt s V s ran i LIdeal R j P | ¬ i j i LIdeal R s = j P | ¬ i j
40 38 39 ax-mp s ran i LIdeal R j P | ¬ i j i LIdeal R s = j P | ¬ i j
41 40 anbi2i s 𝒫 P s ran i LIdeal R j P | ¬ i j s 𝒫 P i LIdeal R s = j P | ¬ i j
42 37 41 bitri s ran i LIdeal R j P | ¬ i j s 𝒫 P i LIdeal R s = j P | ¬ i j
43 rabid s s 𝒫 P | P s ran V s 𝒫 P P s ran V
44 28 42 43 3bitr4g R Ring s ran i LIdeal R j P | ¬ i j s s 𝒫 P | P s ran V
45 9 10 11 44 eqrd R Ring ran i LIdeal R j P | ¬ i j = s 𝒫 P | P s ran V
46 8 45 eqtrd R Ring J = s 𝒫 P | P s ran V