Definition df-rgspn 18779

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 18777	. 2 class RingSpan
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1482	. . . . . 6 class w
6		cbs 15857	. . . . . 6 class Base
7	5, 6	cfv 5888	. . . . 5 class ( Base ` w )
8	7	cpw 4158	. . . 4 class ~P ( Base ` w )
9	4	cv 1482	. . . . . . 7 class s
10		vt	. . . . . . . 8 setvar t
11	10	cv 1482	. . . . . . 7 class t
12	9, 11	wss 3574	. . . . . 6 wff s C_ t
13		csubrg 18776	. . . . . . 7 class SubRing
14	5, 13	cfv 5888	. . . . . 6 class (SubRing ` w )
15	12, 10, 14	crab 2916	. . . . 5 class { t e. (SubRing ` w ) | s C_ t }
16	15	cint 4475	. . . 4 class |^| { t e. (SubRing ` w ) | s C_ t }
17	4, 8, 16	cmpt 4729	. . 3 class ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } )
18	2, 3, 17	cmpt 4729	. 2 class ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
19	1, 18	wceq 1483	1 wff RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )

This definition is referenced by:  rgspnval  37738