Metamath Proof Explorer


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 ( 𝜑𝐴𝑈 )