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 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
zartop.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
Assertion zart0 ( 𝑅 ∈ CRing → 𝐽 ∈ Kol2 )

Proof

Step Hyp Ref Expression
1 zartop.1 ⊢ 𝑆 = ( Spec ‘ 𝑅 )
2 zartop.2 ⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
3 1 2 zartop ⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ Top )
4 sseq2 ⊢ ( 𝑗 = 𝑥 → ( 𝑥 ⊆ 𝑗 ↔ 𝑥 ⊆ 𝑥 ) )
5 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) )
6 ssidd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑥 ⊆ 𝑥 )
7 4 5 6 elrabd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } )
8 7 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) → 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } )
9 sseq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ⊆ 𝑗 ↔ 𝑖 ⊆ 𝑗 ) )
10 9 rabbidv ⊢ ( 𝑘 = 𝑖 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
11 10 cbvmptv ⊢ ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
12 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
13 12 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
14 simplr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) )
15 prmidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑥 ∈ ( LIdeal ‘ 𝑅 ) )
16 13 14 15 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑥 ∈ ( LIdeal ‘ 𝑅 ) )
17 fvex ⊢ ( PrmIdeal ‘ 𝑅 ) ∈ V
18 17 rabex ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ∈ V
19 18 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ∈ V )
20 sseq1 ⊢ ( 𝑖 = 𝑥 → ( 𝑖 ⊆ 𝑗 ↔ 𝑥 ⊆ 𝑗 ) )
21 20 rabbidv ⊢ ( 𝑖 = 𝑥 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } )
22 21 eqcomd ⊢ ( 𝑖 = 𝑥 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
23 22 adantl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑖 = 𝑥 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
24 11 16 19 23 elrnmptdv ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) )
25 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ) → 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } )
26 25 eleq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ) → ( 𝑥 ∈ 𝑑 ↔ 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ) )
27 25 eleq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ) → ( 𝑦 ∈ 𝑑 ↔ 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ) )
28 26 27 bibi12d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ) → ( ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ↔ ( 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ↔ 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ) ) )
29 24 28 rspcdv ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → ( 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ↔ 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ) ) )
30 29 imp ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) → ( 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ↔ 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ) )
31 8 30 mpbid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) → 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } )
32 sseq2 ⊢ ( 𝑗 = 𝑦 → ( 𝑥 ⊆ 𝑗 ↔ 𝑥 ⊆ 𝑦 ) )
33 32 elrab ⊢ ( 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } ↔ ( 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ 𝑥 ⊆ 𝑦 ) )
34 33 simprbi ⊢ ( 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑥 ⊆ 𝑗 } → 𝑥 ⊆ 𝑦 )
35 31 34 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) → 𝑥 ⊆ 𝑦 )
36 sseq2 ⊢ ( 𝑗 = 𝑦 → ( 𝑦 ⊆ 𝑗 ↔ 𝑦 ⊆ 𝑦 ) )
37 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) )
38 ssidd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑦 ⊆ 𝑦 )
39 36 37 38 elrabd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } )
40 39 ad4ant13 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) → 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } )
41 simpr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) )
42 prmidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑦 ∈ ( LIdeal ‘ 𝑅 ) )
43 13 41 42 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑦 ∈ ( LIdeal ‘ 𝑅 ) )
44 17 rabex ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ∈ V
45 44 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ∈ V )
46 sseq1 ⊢ ( 𝑖 = 𝑦 → ( 𝑖 ⊆ 𝑗 ↔ 𝑦 ⊆ 𝑗 ) )
47 46 rabbidv ⊢ ( 𝑖 = 𝑦 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } )
48 47 eqcomd ⊢ ( 𝑖 = 𝑦 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
49 48 adantl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑖 = 𝑦 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
50 11 43 45 49 elrnmptdv ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) )
51 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ) → 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } )
52 51 eleq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ) → ( 𝑥 ∈ 𝑑 ↔ 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ) )
53 51 eleq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ) → ( 𝑦 ∈ 𝑑 ↔ 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ) )
54 52 53 bibi12d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑑 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ) → ( ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ↔ ( 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ↔ 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ) ) )
55 50 54 rspcdv ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → ( 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ↔ 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ) ) )
56 55 imp ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) → ( 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ↔ 𝑦 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ) )
57 40 56 mpbird ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) → 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } )
58 sseq2 ⊢ ( 𝑗 = 𝑥 → ( 𝑦 ⊆ 𝑗 ↔ 𝑦 ⊆ 𝑥 ) )
59 58 elrab ⊢ ( 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } ↔ ( 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ 𝑦 ⊆ 𝑥 ) )
60 59 simprbi ⊢ ( 𝑥 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑦 ⊆ 𝑗 } → 𝑦 ⊆ 𝑥 )
61 57 60 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) → 𝑦 ⊆ 𝑥 )
62 35 61 eqssd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) → 𝑥 = 𝑦 )
63 62 ex ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) )
64 63 anasss ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ) ) → ( ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) )
65 64 ralrimivva ⊢ ( 𝑅 ∈ CRing → ∀ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ∀ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ( ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) )
66 3 65 jca ⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ∀ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ( ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) ) )
67 eqid ⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
68 1 2 67 zartopon ⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) )
69 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) → ( PrmIdeal ‘ 𝑅 ) = ∪ 𝐽 )
70 68 69 syl ⊢ ( 𝑅 ∈ CRing → ( PrmIdeal ‘ 𝑅 ) = ∪ 𝐽 )
71 1 2 67 11 zartopn ⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ ( TopOn ‘ ( PrmIdeal ‘ 𝑅 ) ) ∧ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) = ( Clsd ‘ 𝐽 ) ) )
72 71 simprd ⊢ ( 𝑅 ∈ CRing → ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) = ( Clsd ‘ 𝐽 ) )
73 70 72 ist0cld ⊢ ( 𝑅 ∈ CRing → ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ( PrmIdeal ‘ 𝑅 ) ∀ 𝑦 ∈ ( PrmIdeal ‘ 𝑅 ) ( ∀ 𝑑 ∈ ran ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } ) ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) ) ) )
74 66 73 mpbird ⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ Kol2 )