rgspnmin

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

Step	Hyp	Ref	Expression
1		rgspnval.r	$⊢ φ \to R \in Ring$
2		rgspnval.b	$⊢ φ \to B = {Base}_{R}$
3		rgspnval.ss	$⊢ φ \to A \subseteq B$
4		rgspnval.n	$⊢ φ \to N = RingSpan (R)$
5		rgspnval.sp	$⊢ φ \to U = N (A)$
6		rgspnmin.sr	$⊢ φ \to S \in SubRing (R)$
7		rgspnmin.ss	$⊢ φ \to A \subseteq S$
8	1 2 3 4 5	rgspnval	$⊢ φ \to U = ⋂ \{t \in SubRing (R) \| A \subseteq t\}$
9		sseq2	$⊢ t = S \to (A \subseteq t \leftrightarrow A \subseteq S)$
10	9	elrab	$⊢ S \in \{t \in SubRing (R) \| A \subseteq t\} \leftrightarrow (S \in SubRing (R) \land A \subseteq S)$
11	6 7 10	sylanbrc	$⊢ φ \to S \in \{t \in SubRing (R) \| A \subseteq t\}$
12		intss1	$⊢ S \in \{t \in SubRing (R) \| A \subseteq t\} \to ⋂ \{t \in SubRing (R) \| A \subseteq t\} \subseteq S$
13	11 12	syl	$⊢ φ \to ⋂ \{t \in SubRing (R) \| A \subseteq t\} \subseteq S$
14	8 13	eqsstrd	$⊢ φ \to U \subseteq S$

Metamath Proof Explorer