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	$$⊢\phi \to R\in \mathrm{Ring}$$
	rgspnval.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
	rgspnval.ss	$$⊢\phi \to A\subseteq B$$
	rgspnval.n	$$⊢\phi \to N=\mathrm{RingSpan}\left(R\right)$$
	rgspnval.sp	$$⊢\phi \to U=N\left(A\right)$$
Assertion	rgspnssid	$$⊢\phi \to A\subseteq U$$

Proof

Step	Hyp	Ref	Expression
1		rgspnval.r	$$⊢\phi \to R\in \mathrm{Ring}$$
2		rgspnval.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
3		rgspnval.ss	$$⊢\phi \to A\subseteq B$$
4		rgspnval.n	$$⊢\phi \to N=\mathrm{RingSpan}\left(R\right)$$
5		rgspnval.sp	$$⊢\phi \to U=N\left(A\right)$$
6		ssintub	$$⊢A\subseteq \bigcap \left\{t\in \mathrm{SubRing}\left(R\right)|A\subseteq t\right\}$$
7	1 2 3 4 5	rgspnval	$$⊢\phi \to U=\bigcap \left\{t\in \mathrm{SubRing}\left(R\right)|A\subseteq t\right\}$$
8	6 7	sseqtrrid	$$⊢\phi \to A\subseteq U$$