Definition df-rgspn

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)

	Ref	Expression
Assertion	df-rgspn	$$⊢\mathrm{RingSpan}=\left(w\in \mathrm{V}⟼\left(s\in 𝒫{\mathrm{Base}}_w⟼\bigcap \left\{t\in \mathrm{SubRing}\left(w\right)|s\subseteq t\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crgspn	$$class\mathrm{RingSpan}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_w$$
8		vt	$$setvart$$
9		csubrg	$$class\mathrm{SubRing}$$
10	5 9	cfv	$$class\mathrm{SubRing}\left(w\right)$$
11	3	cv	$$setvars$$
12	8	cv	$$setvart$$
13	11 12	wss	$$wffs\subseteq t$$
14	13 8 10	crab	$$class\left\{t\in \mathrm{SubRing}\left(w\right)|s\subseteq t\right\}$$
15	14	cint	$$class\bigcap \left\{t\in \mathrm{SubRing}\left(w\right)|s\subseteq t\right\}$$
16	3 7 15	cmpt	$$class\left(s\in 𝒫{\mathrm{Base}}_w⟼\bigcap \left\{t\in \mathrm{SubRing}\left(w\right)|s\subseteq t\right\}\right)$$
17	1 2 16	cmpt	$$class\left(w\in \mathrm{V}⟼\left(s\in 𝒫{\mathrm{Base}}_w⟼\bigcap \left\{t\in \mathrm{SubRing}\left(w\right)|s\subseteq t\right\}\right)\right)$$
18	0 17	wceq	$$wff\mathrm{RingSpan}=\left(w\in \mathrm{V}⟼\left(s\in 𝒫{\mathrm{Base}}_w⟼\bigcap \left\{t\in \mathrm{SubRing}\left(w\right)|s\subseteq t\right\}\right)\right)$$