Definition df-csring

Description: Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025)

	Ref	Expression
Assertion	df-csring	⊢ CSRing = { 𝑓 ∈ SRing ∣ ( mulGrp ‘ 𝑓 ) ∈ CMnd }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccsrg	⊢ CSRing
1		vf	⊢ 𝑓
2		csrg	⊢ SRing
3		cmgp	⊢ mulGrp
4	1	cv	⊢ 𝑓
5	4 3	cfv	⊢ ( mulGrp ‘ 𝑓 )
6		ccmn	⊢ CMnd
7	5 6	wcel	⊢ ( mulGrp ‘ 𝑓 ) ∈ CMnd
8	7 1 2	crab	⊢ { 𝑓 ∈ SRing ∣ ( mulGrp ‘ 𝑓 ) ∈ CMnd }
9	0 8	wceq	⊢ CSRing = { 𝑓 ∈ SRing ∣ ( mulGrp ‘ 𝑓 ) ∈ CMnd }