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	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	rgspnval.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
	rgspnval.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	rgspnval.n	⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
	rgspnval.sp	⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ 𝐴 ) )
Assertion	rgspnssid	⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		rgspnval.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
2		rgspnval.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
3		rgspnval.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
4		rgspnval.n	⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
5		rgspnval.sp	⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ 𝐴 ) )
6		ssintub	⊢ 𝐴 ⊆ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 }
7	1 2 3 4 5	rgspnval	⊢ ( 𝜑 → 𝑈 = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )
8	6 7	sseqtrrid	⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )