Theorem rgspnmin

Description: The ring-span is contained in all subrings which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Hypotheses	rgspnval.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	rgspnval.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
	rgspnval.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	rgspnval.n	⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
	rgspnval.sp	⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ 𝐴 ) )
	rgspnmin.sr	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	rgspnmin.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
Assertion	rgspnmin	⊢ ( 𝜑 → 𝑈 ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		rgspnval.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
2		rgspnval.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
3		rgspnval.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
4		rgspnval.n	⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
5		rgspnval.sp	⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ 𝐴 ) )
6		rgspnmin.sr	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7		rgspnmin.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
8	1 2 3 4 5	rgspnval	⊢ ( 𝜑 → 𝑈 = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )
9		sseq2	⊢ ( 𝑡 = 𝑆 → ( 𝐴 ⊆ 𝑡 ↔ 𝐴 ⊆ 𝑆 ) )
10	9	elrab	⊢ ( 𝑆 ∈ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ↔ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐴 ⊆ 𝑆 ) )
11	6 7 10	sylanbrc	⊢ ( 𝜑 → 𝑆 ∈ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )
12		intss1	⊢ ( 𝑆 ∈ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } → ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ⊆ 𝑆 )
13	11 12	syl	⊢ ( 𝜑 → ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ⊆ 𝑆 )
14	8 13	eqsstrd	⊢ ( 𝜑 → 𝑈 ⊆ 𝑆 )