Metamath Proof Explorer

Theorem zart0

Description: The Zariski topology is T_0 . Corollary 1.1.8 of EGA p. 81. (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zartop.1 
|- S = ( Spec ` R )
zartop.2 
|- J = ( TopOpen ` S )
Assertion zart0 
|- ( R e. CRing -> J e. Kol2 )

Proof

Step Hyp Ref Expression
1 zartop.1 
 |-  S = ( Spec ` R )
2 zartop.2 
 |-  J = ( TopOpen ` S )
3 1 2 zartop 
 |-  ( R e. CRing -> J e. Top )
4 sseq2 
 |-  ( j = x -> ( x C_ j <-> x C_ x ) )
5 simpr 
 |-  ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) -> x e. ( PrmIdeal ` R ) )
6 ssidd 
 |-  ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) -> x C_ x )
7 4 5 6 elrabd 
 |-  ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) -> x e. { j e. ( PrmIdeal ` R ) | x C_ j } )
8 7 ad2antrr 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) ) -> x e. { j e. ( PrmIdeal ` R ) | x C_ j } )
9 sseq1 
 |-  ( k = i -> ( k C_ j <-> i C_ j ) )
10 9 rabbidv 
 |-  ( k = i -> { j e. ( PrmIdeal ` R ) | k C_ j } = { j e. ( PrmIdeal ` R ) | i C_ j } )
11 10 cbvmptv 
 |-  ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
12 crngring 
 |-  ( R e. CRing -> R e. Ring )
13 12 ad2antrr 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> R e. Ring )
14 simplr 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> x e. ( PrmIdeal ` R ) )
15 prmidlidl 
 |-  ( ( R e. Ring /\ x e. ( PrmIdeal ` R ) ) -> x e. ( LIdeal ` R ) )
16 13 14 15 syl2anc 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> x e. ( LIdeal ` R ) )
17 fvex 
 |-  ( PrmIdeal ` R ) e. _V
18 17 rabex 
 |-  { j e. ( PrmIdeal ` R ) | x C_ j } e. _V
19 18 a1i 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | x C_ j } e. _V )
20 sseq1 
 |-  ( i = x -> ( i C_ j <-> x C_ j ) )
21 20 rabbidv 
 |-  ( i = x -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | x C_ j } )
22 21 eqcomd 
 |-  ( i = x -> { j e. ( PrmIdeal ` R ) | x C_ j } = { j e. ( PrmIdeal ` R ) | i C_ j } )
23 22 adantl 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ i = x ) -> { j e. ( PrmIdeal ` R ) | x C_ j } = { j e. ( PrmIdeal ` R ) | i C_ j } )
24 11 16 19 23 elrnmptdv 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | x C_ j } e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) )
25 simpr 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ d = { j e. ( PrmIdeal ` R ) | x C_ j } ) -> d = { j e. ( PrmIdeal ` R ) | x C_ j } )
26 25 eleq2d 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ d = { j e. ( PrmIdeal ` R ) | x C_ j } ) -> ( x e. d <-> x e. { j e. ( PrmIdeal ` R ) | x C_ j } ) )
27 25 eleq2d 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ d = { j e. ( PrmIdeal ` R ) | x C_ j } ) -> ( y e. d <-> y e. { j e. ( PrmIdeal ` R ) | x C_ j } ) )
28 26 27 bibi12d 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ d = { j e. ( PrmIdeal ` R ) | x C_ j } ) -> ( ( x e. d <-> y e. d ) <-> ( x e. { j e. ( PrmIdeal ` R ) | x C_ j } <-> y e. { j e. ( PrmIdeal ` R ) | x C_ j } ) ) )
29 24 28 rspcdv 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> ( A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) -> ( x e. { j e. ( PrmIdeal ` R ) | x C_ j } <-> y e. { j e. ( PrmIdeal ` R ) | x C_ j } ) ) )
30 29 imp 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) ) -> ( x e. { j e. ( PrmIdeal ` R ) | x C_ j } <-> y e. { j e. ( PrmIdeal ` R ) | x C_ j } ) )
31 8 30 mpbid 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) ) -> y e. { j e. ( PrmIdeal ` R ) | x C_ j } )
32 sseq2 
 |-  ( j = y -> ( x C_ j <-> x C_ y ) )
33 32 elrab 
 |-  ( y e. { j e. ( PrmIdeal ` R ) | x C_ j } <-> ( y e. ( PrmIdeal ` R ) /\ x C_ y ) )
34 33 simprbi 
 |-  ( y e. { j e. ( PrmIdeal ` R ) | x C_ j } -> x C_ y )
35 31 34 syl 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) ) -> x C_ y )
36 sseq2 
 |-  ( j = y -> ( y C_ j <-> y C_ y ) )
37 simpr 
 |-  ( ( R e. CRing /\ y e. ( PrmIdeal ` R ) ) -> y e. ( PrmIdeal ` R ) )
38 ssidd 
 |-  ( ( R e. CRing /\ y e. ( PrmIdeal ` R ) ) -> y C_ y )
39 36 37 38 elrabd 
 |-  ( ( R e. CRing /\ y e. ( PrmIdeal ` R ) ) -> y e. { j e. ( PrmIdeal ` R ) | y C_ j } )
40 39 ad4ant13 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) ) -> y e. { j e. ( PrmIdeal ` R ) | y C_ j } )
41 simpr 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> y e. ( PrmIdeal ` R ) )
42 prmidlidl 
 |-  ( ( R e. Ring /\ y e. ( PrmIdeal ` R ) ) -> y e. ( LIdeal ` R ) )
43 13 41 42 syl2anc 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> y e. ( LIdeal ` R ) )
44 17 rabex 
 |-  { j e. ( PrmIdeal ` R ) | y C_ j } e. _V
45 44 a1i 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | y C_ j } e. _V )
46 sseq1 
 |-  ( i = y -> ( i C_ j <-> y C_ j ) )
47 46 rabbidv 
 |-  ( i = y -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | y C_ j } )
48 47 eqcomd 
 |-  ( i = y -> { j e. ( PrmIdeal ` R ) | y C_ j } = { j e. ( PrmIdeal ` R ) | i C_ j } )
49 48 adantl 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ i = y ) -> { j e. ( PrmIdeal ` R ) | y C_ j } = { j e. ( PrmIdeal ` R ) | i C_ j } )
50 11 43 45 49 elrnmptdv 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | y C_ j } e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) )
51 simpr 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ d = { j e. ( PrmIdeal ` R ) | y C_ j } ) -> d = { j e. ( PrmIdeal ` R ) | y C_ j } )
52 51 eleq2d 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ d = { j e. ( PrmIdeal ` R ) | y C_ j } ) -> ( x e. d <-> x e. { j e. ( PrmIdeal ` R ) | y C_ j } ) )
53 51 eleq2d 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ d = { j e. ( PrmIdeal ` R ) | y C_ j } ) -> ( y e. d <-> y e. { j e. ( PrmIdeal ` R ) | y C_ j } ) )
54 52 53 bibi12d 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ d = { j e. ( PrmIdeal ` R ) | y C_ j } ) -> ( ( x e. d <-> y e. d ) <-> ( x e. { j e. ( PrmIdeal ` R ) | y C_ j } <-> y e. { j e. ( PrmIdeal ` R ) | y C_ j } ) ) )
55 50 54 rspcdv 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> ( A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) -> ( x e. { j e. ( PrmIdeal ` R ) | y C_ j } <-> y e. { j e. ( PrmIdeal ` R ) | y C_ j } ) ) )
56 55 imp 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) ) -> ( x e. { j e. ( PrmIdeal ` R ) | y C_ j } <-> y e. { j e. ( PrmIdeal ` R ) | y C_ j } ) )
57 40 56 mpbird 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) ) -> x e. { j e. ( PrmIdeal ` R ) | y C_ j } )
58 sseq2 
 |-  ( j = x -> ( y C_ j <-> y C_ x ) )
59 58 elrab 
 |-  ( x e. { j e. ( PrmIdeal ` R ) | y C_ j } <-> ( x e. ( PrmIdeal ` R ) /\ y C_ x ) )
60 59 simprbi 
 |-  ( x e. { j e. ( PrmIdeal ` R ) | y C_ j } -> y C_ x )
61 57 60 syl 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) ) -> y C_ x )
62 35 61 eqssd 
 |-  ( ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) /\ A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) ) -> x = y )
63 62 ex 
 |-  ( ( ( R e. CRing /\ x e. ( PrmIdeal ` R ) ) /\ y e. ( PrmIdeal ` R ) ) -> ( A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) -> x = y ) )
64 63 anasss 
 |-  ( ( R e. CRing /\ ( x e. ( PrmIdeal ` R ) /\ y e. ( PrmIdeal ` R ) ) ) -> ( A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) -> x = y ) )
65 64 ralrimivva 
 |-  ( R e. CRing -> A. x e. ( PrmIdeal ` R ) A. y e. ( PrmIdeal ` R ) ( A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) -> x = y ) )
66 3 65 jca 
 |-  ( R e. CRing -> ( J e. Top /\ A. x e. ( PrmIdeal ` R ) A. y e. ( PrmIdeal ` R ) ( A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) -> x = y ) ) )
67 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
68 1 2 67 zartopon 
 |-  ( R e. CRing -> J e. ( TopOn ` ( PrmIdeal ` R ) ) )
69 toponuni 
 |-  ( J e. ( TopOn ` ( PrmIdeal ` R ) ) -> ( PrmIdeal ` R ) = U. J )
70 68 69 syl 
 |-  ( R e. CRing -> ( PrmIdeal ` R ) = U. J )
71 1 2 67 11 zartopn 
 |-  ( R e. CRing -> ( J e. ( TopOn ` ( PrmIdeal ` R ) ) /\ ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) = ( Clsd ` J ) ) )
72 71 simprd 
 |-  ( R e. CRing -> ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) = ( Clsd ` J ) )
73 70 72 ist0cld 
 |-  ( R e. CRing -> ( J e. Kol2 <-> ( J e. Top /\ A. x e. ( PrmIdeal ` R ) A. y e. ( PrmIdeal ` R ) ( A. d e. ran ( k e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | k C_ j } ) ( x e. d <-> y e. d ) -> x = y ) ) ) )
74 66 73 mpbird 
 |-  ( R e. CRing -> J e. Kol2 )