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 = ( Base ` F )
	fldgenval.2	|- ( ph -> F e. DivRing )
	fldgenval.3	|- ( ph -> S C_ B )
Assertion	fldgenssv	|- ( ph -> ( F fldGen S ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	|- B = ( Base ` F )
2		fldgenval.2	|- ( ph -> F e. DivRing )
3		fldgenval.3	|- ( ph -> S C_ B )
4	1 2 3	fldgenval	|- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )
5		sseq2	|- ( a = B -> ( S C_ a <-> S C_ B ) )
6	1	sdrgid	|- ( F e. DivRing -> B e. ( SubDRing ` F ) )
7	2 6	syl	|- ( ph -> B e. ( SubDRing ` F ) )
8	5 7 3	elrabd	|- ( ph -> B e. { a e. ( SubDRing ` F ) | S C_ a } )
9		intss1	|- ( B e. { a e. ( SubDRing ` F ) | S C_ a } -> |^| { a e. ( SubDRing ` F ) | S C_ a } C_ B )
10	8 9	syl	|- ( ph -> |^| { a e. ( SubDRing ` F ) | S C_ a } C_ B )
11	4 10	eqsstrd	|- ( ph -> ( F fldGen S ) C_ B )