Theorem zarcmp

Description: The Zariski topology is compact. Proposition 1.1.10(ii) of EGA, p. 82. (Contributed by Thierry Arnoux, 2-Jul-2024)

	Ref	Expression
Hypotheses	zartop.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
	zartop.2	⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
Assertion	zarcmp	⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ Comp )

Proof

Step	Hyp	Ref	Expression
1		zartop.1	⊢ 𝑆 = ( Spec ‘ 𝑅 )
2		zartop.2	⊢ 𝐽 = ( TopOpen ‘ 𝑆 )
3		sseq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑗 ) )
4	3	rabbidv	⊢ ( 𝑖 = 𝑘 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } )
5		sseq2	⊢ ( 𝑗 = 𝑙 → ( 𝑘 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑙 ) )
6	5	cbvrabv	⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑗 } = { 𝑙 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑙 }
7	4 6	eqtrdi	⊢ ( 𝑖 = 𝑘 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑙 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑙 } )
8	7	cbvmptv	⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) = ( 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑙 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑘 ⊆ 𝑙 } )
9	1 2 8	zarcmplem	⊢ ( 𝑅 ∈ CRing → 𝐽 ∈ Comp )