Theorem rgspnssid

Description: The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Hypotheses	rgspnval.r	|- ( ph -> R e. Ring )
	rgspnval.b	|- ( ph -> B = ( Base ` R ) )
	rgspnval.ss	|- ( ph -> A C_ B )
	rgspnval.n	|- ( ph -> N = ( RingSpan ` R ) )
	rgspnval.sp	|- ( ph -> U = ( N ` A ) )
Assertion	rgspnssid	|- ( ph -> A C_ U )

Proof

Step	Hyp	Ref	Expression
1		rgspnval.r	|- ( ph -> R e. Ring )
2		rgspnval.b	|- ( ph -> B = ( Base ` R ) )
3		rgspnval.ss	|- ( ph -> A C_ B )
4		rgspnval.n	|- ( ph -> N = ( RingSpan ` R ) )
5		rgspnval.sp	|- ( ph -> U = ( N ` A ) )
6		ssintub	|- A C_ |^| { t e. ( SubRing ` R ) | A C_ t }
7	1 2 3 4 5	rgspnval	|- ( ph -> U = |^| { t e. ( SubRing ` R ) | A C_ t } )
8	6 7	sseqtrrid	|- ( ph -> A C_ U )