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	⊢ 𝑆 = ( Spec ‘ 𝑅 )
	zartop.2	⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
	zarcls.1	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
	zarcls.2	⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } )
Assertion	zarcls	⊢ ( 𝑅 ∈ Ring → 𝐽 = { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } )

Proof

Step	Hyp	Ref	Expression
1		zartop.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
2		zartop.2	⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
3		zarcls.1	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
4		zarcls.2	⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } )
5		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
6		eqid	⊢ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
7	1 5 3 6	rspectopn	⊢ ( 𝑅 ∈ Ring → ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( TopOpen ‘ 𝑆 ) )
8	2 7	eqtr4id	⊢ ( 𝑅 ∈ Ring → 𝐽 = ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
9		nfv	⊢ Ⅎ 𝑠 𝑅 ∈ Ring
10		nfcv	⊢ Ⅎ 𝑠 ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
11		nfrab1	⊢ Ⅎ 𝑠 { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 }
12		notrab	⊢ ( 𝑃 ∖ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 }
13	12	eqeq2i	⊢ ( 𝑠 = ( 𝑃 ∖ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) ↔ 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
14		ssrab2	⊢ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ⊆ 𝑃
15	14	a1i	⊢ ( 𝑠 ∈ 𝒫 𝑃 → { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ⊆ 𝑃 )
16		elpwi	⊢ ( 𝑠 ∈ 𝒫 𝑃 → 𝑠 ⊆ 𝑃 )
17		ssdifsym	⊢ ( ( { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ⊆ 𝑃 ∧ 𝑠 ⊆ 𝑃 ) → ( 𝑠 = ( 𝑃 ∖ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) ↔ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } = ( 𝑃 ∖ 𝑠 ) ) )
18	15 16 17	syl2anc	⊢ ( 𝑠 ∈ 𝒫 𝑃 → ( 𝑠 = ( 𝑃 ∖ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) ↔ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } = ( 𝑃 ∖ 𝑠 ) ) )
19		eqcom	⊢ ( { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } = ( 𝑃 ∖ 𝑠 ) ↔ ( 𝑃 ∖ 𝑠 ) = { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } )
20	18 19	bitrdi	⊢ ( 𝑠 ∈ 𝒫 𝑃 → ( 𝑠 = ( 𝑃 ∖ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) ↔ ( 𝑃 ∖ 𝑠 ) = { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) )
21	13 20	bitr3id	⊢ ( 𝑠 ∈ 𝒫 𝑃 → ( 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ↔ ( 𝑃 ∖ 𝑠 ) = { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) )
22	21	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑠 ∈ 𝒫 𝑃 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ↔ ( 𝑃 ∖ 𝑠 ) = { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) )
23	22	rexbidva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑠 ∈ 𝒫 𝑃 ) → ( ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ↔ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑃 ∖ 𝑠 ) = { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ) )
24	3	fvexi	⊢ 𝑃 ∈ V
25	24	rabex	⊢ { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } ∈ V
26	4 25	elrnmpti	⊢ ( ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 ↔ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑃 ∖ 𝑠 ) = { 𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗 } )
27	23 26	bitr4di	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑠 ∈ 𝒫 𝑃 ) → ( ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ↔ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 ) )
28	27	pm5.32da	⊢ ( 𝑅 ∈ Ring → ( ( 𝑠 ∈ 𝒫 𝑃 ∧ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↔ ( 𝑠 ∈ 𝒫 𝑃 ∧ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 ) ) )
29		ssrab2	⊢ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ⊆ 𝑃
30	24	elpw2	⊢ ( { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ 𝒫 𝑃 ↔ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ⊆ 𝑃 )
31	29 30	mpbir	⊢ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ 𝒫 𝑃
32	31	rgenw	⊢ ∀ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ 𝒫 𝑃
33		eqid	⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
34	33	rnmptss	⊢ ( ∀ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ∈ 𝒫 𝑃 → ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⊆ 𝒫 𝑃 )
35	32 34	ax-mp	⊢ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ⊆ 𝒫 𝑃
36	35	sseli	⊢ ( 𝑠 ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) → 𝑠 ∈ 𝒫 𝑃 )
37	36	pm4.71ri	⊢ ( 𝑠 ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↔ ( 𝑠 ∈ 𝒫 𝑃 ∧ 𝑠 ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ) )
38		vex	⊢ 𝑠 ∈ V
39	33	elrnmpt	⊢ ( 𝑠 ∈ V → ( 𝑠 ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↔ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
40	38 39	ax-mp	⊢ ( 𝑠 ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↔ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } )
41	40	anbi2i	⊢ ( ( 𝑠 ∈ 𝒫 𝑃 ∧ 𝑠 ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ) ↔ ( 𝑠 ∈ 𝒫 𝑃 ∧ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
42	37 41	bitri	⊢ ( 𝑠 ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↔ ( 𝑠 ∈ 𝒫 𝑃 ∧ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) 𝑠 = { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) )
43		rabid	⊢ ( 𝑠 ∈ { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } ↔ ( 𝑠 ∈ 𝒫 𝑃 ∧ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 ) )
44	28 42 43	3bitr4g	⊢ ( 𝑅 ∈ Ring → ( 𝑠 ∈ ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) ↔ 𝑠 ∈ { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } ) )
45	9 10 11 44	eqrd	⊢ ( 𝑅 ∈ Ring → ran ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗 } ) = { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } )
46	8 45	eqtrd	⊢ ( 𝑅 ∈ Ring → 𝐽 = { 𝑠 ∈ 𝒫 𝑃 ∣ ( 𝑃 ∖ 𝑠 ) ∈ ran 𝑉 } )