This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → R ∈ Ring
rgspnval.b ⊢ φ → B = Base R
rgspnval.ss ⊢ φ → A ⊆ B
rgspnval.n ⊢ φ → N = RingSpan ⁡ R
rgspnval.sp ⊢ φ → U = N ⁡ A
Assertion rgspnssid ⊢ φ → A ⊆ U

Proof

Step Hyp Ref Expression
1 rgspnval.r ⊢ φ → R ∈ Ring
2 rgspnval.b ⊢ φ → B = Base R
3 rgspnval.ss ⊢ φ → A ⊆ B
4 rgspnval.n ⊢ φ → N = RingSpan ⁡ R
5 rgspnval.sp ⊢ φ → U = N ⁡ A
6 ssintub ⊢ A ⊆ ⋂ t ∈ SubRing ⁡ R | A ⊆ t
7 1 2 3 4 5 rgspnval ⊢ φ → U = ⋂ t ∈ SubRing ⁡ R | A ⊆ t
8 6 7 sseqtrrid ⊢ φ → A ⊆ U