Theorem rspectopn

Description: The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024)

	Ref	Expression
Hypotheses	rspecbas.1	No typesetting found for |- S = ( Spec ` R ) with typecode |-
	rspectopn.1	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
	rspectopn.2	No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
	rspectopn.3	$$⊢J=\mathrm{ran}\left(i\in I⟼\left\{j\in P|\neg i\subseteq j\right\}\right)$$
Assertion	rspectopn	$$⊢R\in \mathrm{Ring}\to J=\mathrm{TopOpen}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		rspecbas.1	Could not format S = ( Spec ` R ) : No typesetting found for |- S = ( Spec ` R ) with typecode |-
2		rspectopn.1	$$⊢I=\mathrm{LIdeal}\left(R\right)$$
3		rspectopn.2	Could not format P = ( PrmIdeal ` R ) : No typesetting found for |- P = ( PrmIdeal ` R ) with typecode |-
4		rspectopn.3	$$⊢J=\mathrm{ran}\left(i\in I⟼\left\{j\in P|\neg i\subseteq j\right\}\right)$$
5		rspecval	Could not format ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ( Spec ` R ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) ) with typecode |-
6	3	oveq2i	Could not format ( ( IDLsrg ` R ) |`s P ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( IDLsrg ` R ) |`s P ) = ( ( IDLsrg ` R ) |`s ( PrmIdeal ` R ) ) with typecode |-
7	5 1 6	3eqtr4g	Could not format ( R e. Ring -> S = ( ( IDLsrg ` R ) |`s P ) ) : No typesetting found for |- ( R e. Ring -> S = ( ( IDLsrg ` R ) |`s P ) ) with typecode |-
8	7	fveq2d	Could not format ( R e. Ring -> ( TopOpen ` S ) = ( TopOpen ` ( ( IDLsrg ` R ) |`s P ) ) ) : No typesetting found for |- ( R e. Ring -> ( TopOpen ` S ) = ( TopOpen ` ( ( IDLsrg ` R ) |`s P ) ) ) with typecode |-
9		eqid	Could not format ( ( IDLsrg ` R ) |`s P ) = ( ( IDLsrg ` R ) |`s P ) : No typesetting found for |- ( ( IDLsrg ` R ) |`s P ) = ( ( IDLsrg ` R ) |`s P ) with typecode |-
10		eqid	Could not format ( TopOpen ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) : No typesetting found for |- ( TopOpen ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) with typecode |-
11	9 10	resstopn	Could not format ( ( TopOpen ` ( IDLsrg ` R ) ) |`t P ) = ( TopOpen ` ( ( IDLsrg ` R ) |`s P ) ) : No typesetting found for |- ( ( TopOpen ` ( IDLsrg ` R ) ) |`t P ) = ( TopOpen ` ( ( IDLsrg ` R ) |`s P ) ) with typecode |-
12	8 11	eqtr4di	Could not format ( R e. Ring -> ( TopOpen ` S ) = ( ( TopOpen ` ( IDLsrg ` R ) ) |`t P ) ) : No typesetting found for |- ( R e. Ring -> ( TopOpen ` S ) = ( ( TopOpen ` ( IDLsrg ` R ) ) |`t P ) ) with typecode |-
13		eqid	Could not format ( IDLsrg ` R ) = ( IDLsrg ` R ) : No typesetting found for |- ( IDLsrg ` R ) = ( IDLsrg ` R ) with typecode |-
14		eqid	$$⊢\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)=\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)$$
15	13 2 14	idlsrgtset	Could not format ( R e. Ring -> ran ( i e. I |-> { j e. I | -. i C_ j } ) = ( TopSet ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ran ( i e. I |-> { j e. I | -. i C_ j } ) = ( TopSet ` ( IDLsrg ` R ) ) ) with typecode |-
16	2	fvexi	$$⊢I\in \mathrm{V}$$
17	16	rabex	$$⊢\left\{j\in I|\neg i\subseteq j\right\}\in \mathrm{V}$$
18	17	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge i\in I\right)\to \left\{j\in I|\neg i\subseteq j\right\}\in \mathrm{V}$$
19		simp2	$$⊢\left(\left(R\in \mathrm{Ring}\wedge i\in I\right)\wedge j\in I\wedge \neg i\subseteq j\right)\to j\in I$$
20	13 2	idlsrgbas	Could not format ( R e. Ring -> I = ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( R e. Ring -> I = ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
21	20	adantr	Could not format ( ( R e. Ring /\ i e. I ) -> I = ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( ( R e. Ring /\ i e. I ) -> I = ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
22	21	3ad2ant1	Could not format ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> I = ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> I = ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
23	19 22	eleqtrd	Could not format ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> j e. ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( ( ( R e. Ring /\ i e. I ) /\ j e. I /\ -. i C_ j ) -> j e. ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
24	23	rabssdv	Could not format ( ( R e. Ring /\ i e. I ) -> { j e. I | -. i C_ j } C_ ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( ( R e. Ring /\ i e. I ) -> { j e. I | -. i C_ j } C_ ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
25	18 24	elpwd	Could not format ( ( R e. Ring /\ i e. I ) -> { j e. I | -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( ( R e. Ring /\ i e. I ) -> { j e. I | -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
26	25	ralrimiva	Could not format ( R e. Ring -> A. i e. I { j e. I | -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( R e. Ring -> A. i e. I { j e. I | -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
27		eqid	$$⊢\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)=\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)$$
28	27	rnmptss	Could not format ( A. i e. I { j e. I | -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) -> ran ( i e. I |-> { j e. I | -. i C_ j } ) C_ ~P ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( A. i e. I { j e. I | -. i C_ j } e. ~P ( Base ` ( IDLsrg ` R ) ) -> ran ( i e. I |-> { j e. I | -. i C_ j } ) C_ ~P ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
29	26 28	syl	Could not format ( R e. Ring -> ran ( i e. I |-> { j e. I | -. i C_ j } ) C_ ~P ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ran ( i e. I |-> { j e. I | -. i C_ j } ) C_ ~P ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
30	15 29	eqsstrrd	Could not format ( R e. Ring -> ( TopSet ` ( IDLsrg ` R ) ) C_ ~P ( Base ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ( TopSet ` ( IDLsrg ` R ) ) C_ ~P ( Base ` ( IDLsrg ` R ) ) ) with typecode |-
31		eqid	Could not format ( Base ` ( IDLsrg ` R ) ) = ( Base ` ( IDLsrg ` R ) ) : No typesetting found for |- ( Base ` ( IDLsrg ` R ) ) = ( Base ` ( IDLsrg ` R ) ) with typecode |-
32		eqid	Could not format ( TopSet ` ( IDLsrg ` R ) ) = ( TopSet ` ( IDLsrg ` R ) ) : No typesetting found for |- ( TopSet ` ( IDLsrg ` R ) ) = ( TopSet ` ( IDLsrg ` R ) ) with typecode |-
33	31 32	topnid	Could not format ( ( TopSet ` ( IDLsrg ` R ) ) C_ ~P ( Base ` ( IDLsrg ` R ) ) -> ( TopSet ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( ( TopSet ` ( IDLsrg ` R ) ) C_ ~P ( Base ` ( IDLsrg ` R ) ) -> ( TopSet ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) ) with typecode |-
34	30 33	syl	Could not format ( R e. Ring -> ( TopSet ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ( TopSet ` ( IDLsrg ` R ) ) = ( TopOpen ` ( IDLsrg ` R ) ) ) with typecode |-
35	15 34	eqtrd	Could not format ( R e. Ring -> ran ( i e. I |-> { j e. I | -. i C_ j } ) = ( TopOpen ` ( IDLsrg ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ran ( i e. I |-> { j e. I | -. i C_ j } ) = ( TopOpen ` ( IDLsrg ` R ) ) ) with typecode |-
36	35	oveq1d	Could not format ( R e. Ring -> ( ran ( i e. I |-> { j e. I | -. i C_ j } ) |`t P ) = ( ( TopOpen ` ( IDLsrg ` R ) ) |`t P ) ) : No typesetting found for |- ( R e. Ring -> ( ran ( i e. I |-> { j e. I | -. i C_ j } ) |`t P ) = ( ( TopOpen ` ( IDLsrg ` R ) ) |`t P ) ) with typecode |-
37	16	mptex	$$⊢\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)\in \mathrm{V}$$
38	37	rnex	$$⊢\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)\in \mathrm{V}$$
39	3	fvexi	$$⊢P\in \mathrm{V}$$
40		elrest	$$⊢\left(\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)\in \mathrm{V}\wedge P\in \mathrm{V}\right)\to \left(x\in \left(\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right){\upharpoonright }_{𝑡}P\right)\leftrightarrow \exists y\in \mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)x=y\cap P\right)$$
41	38 39 40	mp2an	$$⊢x\in \left(\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right){\upharpoonright }_{𝑡}P\right)\leftrightarrow \exists y\in \mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)x=y\cap P$$
42	17	rgenw	$$⊢\forall i\in I\left\{j\in I|\neg i\subseteq j\right\}\in \mathrm{V}$$
43		ineq1	$$⊢y=\left\{j\in I|\neg i\subseteq j\right\}\to y\cap P=\left\{j\in I|\neg i\subseteq j\right\}\cap P$$
44	43	eqeq2d	$$⊢y=\left\{j\in I|\neg i\subseteq j\right\}\to \left(x=y\cap P\leftrightarrow x=\left\{j\in I|\neg i\subseteq j\right\}\cap P\right)$$
45	27 44	rexrnmptw	$$⊢\forall i\in I\left\{j\in I|\neg i\subseteq j\right\}\in \mathrm{V}\to \left(\exists y\in \mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)x=y\cap P\leftrightarrow \exists i\in Ix=\left\{j\in I|\neg i\subseteq j\right\}\cap P\right)$$
46	42 45	ax-mp	$$⊢\exists y\in \mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)x=y\cap P\leftrightarrow \exists i\in Ix=\left\{j\in I|\neg i\subseteq j\right\}\cap P$$
47		inrab2	$$⊢\left\{j\in I|\neg i\subseteq j\right\}\cap P=\left\{j\in \left(I\cap P\right)|\neg i\subseteq j\right\}$$
48		prmidlssidl	Could not format ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |-
49	48 3 2	3sstr4g	$$⊢R\in \mathrm{Ring}\to P\subseteq I$$
50		sseqin2	$$⊢P\subseteq I\leftrightarrow I\cap P=P$$
51	49 50	sylib	$$⊢R\in \mathrm{Ring}\to I\cap P=P$$
52	51	rabeqdv	$$⊢R\in \mathrm{Ring}\to \left\{j\in \left(I\cap P\right)|\neg i\subseteq j\right\}=\left\{j\in P|\neg i\subseteq j\right\}$$
53	47 52	eqtrid	$$⊢R\in \mathrm{Ring}\to \left\{j\in I|\neg i\subseteq j\right\}\cap P=\left\{j\in P|\neg i\subseteq j\right\}$$
54	53	eqeq2d	$$⊢R\in \mathrm{Ring}\to \left(x=\left\{j\in I|\neg i\subseteq j\right\}\cap P\leftrightarrow x=\left\{j\in P|\neg i\subseteq j\right\}\right)$$
55	54	rexbidv	$$⊢R\in \mathrm{Ring}\to \left(\exists i\in Ix=\left\{j\in I|\neg i\subseteq j\right\}\cap P\leftrightarrow \exists i\in Ix=\left\{j\in P|\neg i\subseteq j\right\}\right)$$
56	46 55	bitrid	$$⊢R\in \mathrm{Ring}\to \left(\exists y\in \mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right)x=y\cap P\leftrightarrow \exists i\in Ix=\left\{j\in P|\neg i\subseteq j\right\}\right)$$
57	41 56	bitrid	$$⊢R\in \mathrm{Ring}\to \left(x\in \left(\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right){\upharpoonright }_{𝑡}P\right)\leftrightarrow \exists i\in Ix=\left\{j\in P|\neg i\subseteq j\right\}\right)$$
58	4	eleq2i	$$⊢x\in J\leftrightarrow x\in \mathrm{ran}\left(i\in I⟼\left\{j\in P|\neg i\subseteq j\right\}\right)$$
59		eqid	$$⊢\left(i\in I⟼\left\{j\in P|\neg i\subseteq j\right\}\right)=\left(i\in I⟼\left\{j\in P|\neg i\subseteq j\right\}\right)$$
60	39	rabex	$$⊢\left\{j\in P|\neg i\subseteq j\right\}\in \mathrm{V}$$
61	59 60	elrnmpti	$$⊢x\in \mathrm{ran}\left(i\in I⟼\left\{j\in P|\neg i\subseteq j\right\}\right)\leftrightarrow \exists i\in Ix=\left\{j\in P|\neg i\subseteq j\right\}$$
62	58 61	bitri	$$⊢x\in J\leftrightarrow \exists i\in Ix=\left\{j\in P|\neg i\subseteq j\right\}$$
63	57 62	bitr4di	$$⊢R\in \mathrm{Ring}\to \left(x\in \left(\mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right){\upharpoonright }_{𝑡}P\right)\leftrightarrow x\in J\right)$$
64	63	eqrdv	$$⊢R\in \mathrm{Ring}\to \mathrm{ran}\left(i\in I⟼\left\{j\in I|\neg i\subseteq j\right\}\right){\upharpoonright }_{𝑡}P=J$$
65	12 36 64	3eqtr2rd	$$⊢R\in \mathrm{Ring}\to J=\mathrm{TopOpen}\left(S\right)$$