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	No typesetting found for |- S = ( Spec ` R ) with typecode |-
	zartop.2	$$⊢J=\mathrm{TopOpen}\left(S\right)$$
Assertion	zart0	$$⊢R\in \mathrm{CRing}\to J\in \mathrm{Kol2}$$

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