Definition df-rgspn 19938

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 19936	. 2 class RingSpan
2		vw	. . 3 setvar 𝑤
3		cvv 3422	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1538	. . . . . 6 class 𝑤
6		cbs 16840	. . . . . 6 class Base
7	5, 6	cfv 6418	. . . . 5 class (Base‘𝑤)
8	7	cpw 4530	. . . 4 class 𝒫 (Base‘𝑤)
9	4	cv 1538	. . . . . . 7 class 𝑠
10		vt	. . . . . . . 8 setvar 𝑡
11	10	cv 1538	. . . . . . 7 class 𝑡
12	9, 11	wss 3883	. . . . . 6 wff 𝑠 ⊆ 𝑡
13		csubrg 19935	. . . . . . 7 class SubRing
14	5, 13	cfv 6418	. . . . . 6 class (SubRing‘𝑤)
15	12, 10, 14	crab 3067	. . . . 5 class {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}
16	15	cint 4876	. . . 4 class ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}
17	4, 8, 16	cmpt 5153	. . 3 class (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡})
18	2, 3, 17	cmpt 5153	. 2 class (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))
19	1, 18	wceq 1539	1 wff RingSpan = (𝑤 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡 ∈ (SubRing‘𝑤) ∣ 𝑠 ⊆ 𝑡}))

This definition is referenced by:  rgspnval  40909