Definition df-rgspn 13852

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 13850	. 2 class RingSpan
2		vw	. . 3 setvar w
3		cvv 2763	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1363	. . . . . 6 class w
6		cbs 12703	. . . . . 6 class Base
7	5, 6	cfv 5259	. . . . 5 class ( Base ` w )
8	7	cpw 3606	. . . 4 class ~P ( Base ` w )
9	4	cv 1363	. . . . . . 7 class s
10		vt	. . . . . . . 8 setvar t
11	10	cv 1363	. . . . . . 7 class t
12	9, 11	wss 3157	. . . . . 6 wff s C_ t
13		csubrg 13849	. . . . . . 7 class SubRing
14	5, 13	cfv 5259	. . . . . 6 class (SubRing ` w )
15	12, 10, 14	crab 2479	. . . . 5 class { t e. (SubRing ` w ) | s C_ t }
16	15	cint 3875	. . . 4 class |^| { t e. (SubRing ` w ) | s C_ t }
17	4, 8, 16	cmpt 4095	. . 3 class ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } )
18	2, 3, 17	cmpt 4095	. 2 class ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
19	1, 18	wceq 1364	1 wff RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )

This definition is referenced by: (None)