Definition df-rgspn 13301

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 = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )

Distinct variable group:   w, s, t

Detailed syntax breakdown of Definition df-rgspn

Step	Hyp	Ref	Expression
1		crgspn 13299	. 2 class RingSpan
2		vw	. . 3 setvar w
3		cvv 2737	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1352	. . . . . 6 class w
6		cbs 12456	. . . . . 6 class Base
7	5, 6	cfv 5216	. . . . 5 class ( Base ` w )
8	7	cpw 3575	. . . 4 class ~P ( Base ` w )
9	4	cv 1352	. . . . . . 7 class s
10		vt	. . . . . . . 8 setvar t
11	10	cv 1352	. . . . . . 7 class t
12	9, 11	wss 3129	. . . . . 6 wff s C_ t
13		csubrg 13298	. . . . . . 7 class SubRing
14	5, 13	cfv 5216	. . . . . 6 class (SubRing ` w )
15	12, 10, 14	crab 2459	. . . . 5 class { t e. (SubRing ` w ) | s C_ t }
16	15	cint 3844	. . . 4 class |^| { t e. (SubRing ` w ) | s C_ t }
17	4, 8, 16	cmpt 4064	. . 3 class ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } )
18	2, 3, 17	cmpt 4064	. 2 class ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
19	1, 18	wceq 1353	1 wff RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )

This definition is referenced by: (None)