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 
|- S = ( Spec ` R )
zartop.2 
|- J = ( TopOpen ` S )
zarcls.1 
|- P = ( PrmIdeal ` R )
zarcls.2 
|- V = ( i e. ( LIdeal ` R ) |-> { j e. P | i C_ j } )
Assertion zarcls 
|- ( R e. Ring -> J = { s e. ~P P | ( P \ s ) e. ran V } )

Proof

Step Hyp Ref Expression
1 zartop.1 
 |-  S = ( Spec ` R )
2 zartop.2 
 |-  J = ( TopOpen ` S )
3 zarcls.1 
 |-  P = ( PrmIdeal ` R )
4 zarcls.2 
 |-  V = ( i e. ( LIdeal ` R ) |-> { j e. P | i C_ j } )
5 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
6 eqid 
 |-  ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) = ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } )
7 1 5 3 6 rspectopn 
 |-  ( R e. Ring -> ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) = ( TopOpen ` S ) )
8 2 7 eqtr4id 
 |-  ( R e. Ring -> J = ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) )
9 nfv 
 |-  F/ s R e. Ring
10 nfcv 
 |-  F/_ s ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } )
11 nfrab1 
 |-  F/_ s { s e. ~P P | ( P \ s ) e. ran V }
12 notrab 
 |-  ( P \ { j e. P | i C_ j } ) = { j e. P | -. i C_ j }
13 12 eqeq2i 
 |-  ( s = ( P \ { j e. P | i C_ j } ) <-> s = { j e. P | -. i C_ j } )
14 ssrab2 
 |-  { j e. P | i C_ j } C_ P
15 14 a1i 
 |-  ( s e. ~P P -> { j e. P | i C_ j } C_ P )
16 elpwi 
 |-  ( s e. ~P P -> s C_ P )
17 ssdifsym 
 |-  ( ( { j e. P | i C_ j } C_ P /\ s C_ P ) -> ( s = ( P \ { j e. P | i C_ j } ) <-> { j e. P | i C_ j } = ( P \ s ) ) )
18 15 16 17 syl2anc 
 |-  ( s e. ~P P -> ( s = ( P \ { j e. P | i C_ j } ) <-> { j e. P | i C_ j } = ( P \ s ) ) )
19 eqcom 
 |-  ( { j e. P | i C_ j } = ( P \ s ) <-> ( P \ s ) = { j e. P | i C_ j } )
20 18 19 bitrdi 
 |-  ( s e. ~P P -> ( s = ( P \ { j e. P | i C_ j } ) <-> ( P \ s ) = { j e. P | i C_ j } ) )
21 13 20 bitr3id 
 |-  ( s e. ~P P -> ( s = { j e. P | -. i C_ j } <-> ( P \ s ) = { j e. P | i C_ j } ) )
22 21 ad2antlr 
 |-  ( ( ( R e. Ring /\ s e. ~P P ) /\ i e. ( LIdeal ` R ) ) -> ( s = { j e. P | -. i C_ j } <-> ( P \ s ) = { j e. P | i C_ j } ) )
23 22 rexbidva 
 |-  ( ( R e. Ring /\ s e. ~P P ) -> ( E. i e. ( LIdeal ` R ) s = { j e. P | -. i C_ j } <-> E. i e. ( LIdeal ` R ) ( P \ s ) = { j e. P | i C_ j } ) )
24 3 fvexi 
 |-  P e. _V
25 24 rabex 
 |-  { j e. P | i C_ j } e. _V
26 4 25 elrnmpti 
 |-  ( ( P \ s ) e. ran V <-> E. i e. ( LIdeal ` R ) ( P \ s ) = { j e. P | i C_ j } )
27 23 26 bitr4di 
 |-  ( ( R e. Ring /\ s e. ~P P ) -> ( E. i e. ( LIdeal ` R ) s = { j e. P | -. i C_ j } <-> ( P \ s ) e. ran V ) )
28 27 pm5.32da 
 |-  ( R e. Ring -> ( ( s e. ~P P /\ E. i e. ( LIdeal ` R ) s = { j e. P | -. i C_ j } ) <-> ( s e. ~P P /\ ( P \ s ) e. ran V ) ) )
29 ssrab2 
 |-  { j e. P | -. i C_ j } C_ P
30 24 elpw2 
 |-  ( { j e. P | -. i C_ j } e. ~P P <-> { j e. P | -. i C_ j } C_ P )
31 29 30 mpbir 
 |-  { j e. P | -. i C_ j } e. ~P P
32 31 rgenw 
 |-  A. i e. ( LIdeal ` R ) { j e. P | -. i C_ j } e. ~P P
33 eqid 
 |-  ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) = ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } )
34 33 rnmptss 
 |-  ( A. i e. ( LIdeal ` R ) { j e. P | -. i C_ j } e. ~P P -> ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) C_ ~P P )
35 32 34 ax-mp 
 |-  ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) C_ ~P P
36 35 sseli 
 |-  ( s e. ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) -> s e. ~P P )
37 36 pm4.71ri 
 |-  ( s e. ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) <-> ( s e. ~P P /\ s e. ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) ) )
38 vex 
 |-  s e. _V
39 33 elrnmpt 
 |-  ( s e. _V -> ( s e. ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) <-> E. i e. ( LIdeal ` R ) s = { j e. P | -. i C_ j } ) )
40 38 39 ax-mp 
 |-  ( s e. ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) <-> E. i e. ( LIdeal ` R ) s = { j e. P | -. i C_ j } )
41 40 anbi2i 
 |-  ( ( s e. ~P P /\ s e. ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) ) <-> ( s e. ~P P /\ E. i e. ( LIdeal ` R ) s = { j e. P | -. i C_ j } ) )
42 37 41 bitri 
 |-  ( s e. ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) <-> ( s e. ~P P /\ E. i e. ( LIdeal ` R ) s = { j e. P | -. i C_ j } ) )
43 rabid 
 |-  ( s e. { s e. ~P P | ( P \ s ) e. ran V } <-> ( s e. ~P P /\ ( P \ s ) e. ran V ) )
44 28 42 43 3bitr4g 
 |-  ( R e. Ring -> ( s e. ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) <-> s e. { s e. ~P P | ( P \ s ) e. ran V } ) )
45 9 10 11 44 eqrd 
 |-  ( R e. Ring -> ran ( i e. ( LIdeal ` R ) |-> { j e. P | -. i C_ j } ) = { s e. ~P P | ( P \ s ) e. ran V } )
46 8 45 eqtrd 
 |-  ( R e. Ring -> J = { s e. ~P P | ( P \ s ) e. ran V } )