Definition df-rspec 31527

Description: Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.)

Assertion

Ref	Expression
df-rspec	⊢ Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟)))

Detailed syntax breakdown of Definition df-rspec

Step	Hyp	Ref	Expression
1		crspec 31526	. 2 class Spec
2		vr	. . 3 setvar 𝑟
3		crg 19562	. . 3 class Ring
4	2	cv 1542	. . . . 5 class 𝑟
5		cidlsrg 31359	. . . . 5 class IDLsrg
6	4, 5	cfv 6380	. . . 4 class (IDLsrg‘𝑟)
7		cprmidl 31324	. . . . 5 class PrmIdeal
8	4, 7	cfv 6380	. . . 4 class (PrmIdeal‘𝑟)
9		cress 16784	. . . 4 class ↾s
10	6, 8, 9	co 7213	. . 3 class ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟))
11	2, 3, 10	cmpt 5135	. 2 class (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟)))
12	1, 11	wceq 1543	1 wff Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟)))

This definition is referenced by:  rspecval  31528