Theorem fldgenssid

Description: The field generated by a set of elements contains those elements. See lspssid . (Contributed by Thierry Arnoux, 15-Jan-2025)

	Ref	Expression
Hypotheses	fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
	fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
	fldgenval.3	$$⊢\phi \to S\subseteq B$$
Assertion	fldgenssid	$$⊢\phi \to S\subseteq F\mathrm{fldGen}S$$

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
2		fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
3		fldgenval.3	$$⊢\phi \to S\subseteq B$$
4		ssintub	$$⊢S\subseteq \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
5	1 2 3	fldgenval	$$⊢\phi \to F\mathrm{fldGen}S=\bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
6	4 5	sseqtrrid	$$⊢\phi \to S\subseteq F\mathrm{fldGen}S$$