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

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
2		fldgenval.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3		fldgenval.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
4	1 2 3	fldgenval	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
5		sseq2	⊢ ( 𝑎 = 𝐵 → ( 𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝐵 ) )
6	1	sdrgid	⊢ ( 𝐹 ∈ DivRing → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
8	5 7 3	elrabd	⊢ ( 𝜑 → 𝐵 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
9		intss1	⊢ ( 𝐵 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ⊆ 𝐵 )
10	8 9	syl	⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ⊆ 𝐵 )
11	4 10	eqsstrd	⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) ⊆ 𝐵 )