Definition df-rgspn 18602

Description: The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.)

Assertion

Ref	Expression
df-rgspn	⊢ RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))

Distinct variable group:   𝑤,𝑠,𝑡

Detailed syntax breakdown of Definition df-rgspn

Step	Hyp	Ref	Expression
1		crgspn 18600	. 2 class RingSpan
2		vw	. . 3 setvar 𝑤
3		cvv 3173	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1474	. . . . . 6 class 𝑤
6		cbs 15695	. . . . . 6 class Base
7	5, 6	cfv 5804	. . . . 5 class (Base‘𝑤)
8	7	cpw 4108	. . . 4 class 𝒫 (Base‘𝑤)
9	4	cv 1474	. . . . . . 7 class 𝑠
10		vt	. . . . . . . 8 setvar 𝑡
11	10	cv 1474	. . . . . . 7 class 𝑡
12	9, 11	wss 3540	. . . . . 6 wff 𝑠 ⊆ 𝑡
13		csubrg 18599	. . . . . . 7 class SubRing
14	5, 13	cfv 5804	. . . . . 6 class (SubRing‘𝑤)
15	12, 10, 14	crab 2900	. . . . 5 class {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}
16	15	cint 4410	. . . 4 class ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}
17	4, 8, 16	cmpt 4643	. . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡})
18	2, 3, 17	cmpt 4643	. 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
19	1, 18	wceq 1475	1 wff RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))

This definition is referenced by:  rgspnval  36757