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

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
2		fldgenval.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3		fldgenval.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
4		ssintub	⊢ 𝑆 ⊆ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 }
5	1 2 3	fldgenval	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
6	4 5	sseqtrrid	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝐹 fldGen 𝑆 ) )