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

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		ssintub	|- S C_ |^| { a e. ( SubDRing ` F ) | S C_ a }
5	1 2 3	fldgenval	|- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )
6	4 5	sseqtrrid	|- ( ph -> S C_ ( F fldGen S ) )