Theorem fldgenid

Description: The subfield of a field F generated by the whole base set of F is F itself. (Contributed by Thierry Arnoux, 11-Jan-2025)

	Ref	Expression
Hypotheses	fldgenval.1	|- B = ( Base ` F )
	fldgenval.2	|- ( ph -> F e. DivRing )
Assertion	fldgenid	|- ( ph -> ( F fldGen B ) = B )

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	|- B = ( Base ` F )
2		fldgenval.2	|- ( ph -> F e. DivRing )
3		ssidd	|- ( ph -> B C_ B )
4	1 2 3	fldgenssv	|- ( ph -> ( F fldGen B ) C_ B )
5	1 2 3	fldgenssid	|- ( ph -> B C_ ( F fldGen B ) )
6	4 5	eqssd	|- ( ph -> ( F fldGen B ) = B )