Theorem fldgenssv

Description: A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-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	fldgenssv	$$⊢\phi \to F\mathrm{fldGen}S\subseteq B$$

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	1 2 3	fldgenval	$$⊢\phi \to F\mathrm{fldGen}S=\bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
5		sseq2	$$⊢a=B\to \left(S\subseteq a\leftrightarrow S\subseteq B\right)$$
6	1	sdrgid	$$⊢F\in \mathrm{DivRing}\to B\in \mathrm{SubDRing}\left(F\right)$$
7	2 6	syl	$$⊢\phi \to B\in \mathrm{SubDRing}\left(F\right)$$
8	5 7 3	elrabd	$$⊢\phi \to B\in \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
9		intss1	$$⊢B\in \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}\to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}\subseteq B$$
10	8 9	syl	$$⊢\phi \to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}\subseteq B$$
11	4 10	eqsstrd	$$⊢\phi \to F\mathrm{fldGen}S\subseteq B$$