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	⊢ 𝐵 = ( Base ‘ 𝐹 )
	fldgenval.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
Assertion	fldgenid	⊢ ( 𝜑 → ( 𝐹 fldGen 𝐵 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
2		fldgenval.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3		ssidd	⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
4	1 2 3	fldgenssv	⊢ ( 𝜑 → ( 𝐹 fldGen 𝐵 ) ⊆ 𝐵 )
5	1 2 3	fldgenssid	⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐹 fldGen 𝐵 ) )
6	4 5	eqssd	⊢ ( 𝜑 → ( 𝐹 fldGen 𝐵 ) = 𝐵 )