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={\mathrm{Base}}_F$$
	fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
	fldgenval.3	$$⊢\phi \to S\subseteq B$$
Assertion	fldgenssid	Could not format assertion : No typesetting found for |- ( ph -> S C_ ( F fldGen S ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
2		fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
3		fldgenval.3	$$⊢\phi \to S\subseteq B$$
4		ssintub	$$⊢S\subseteq \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
5	1 2 3	fldgenval	Could not format ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) : No typesetting found for |- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) with typecode |-
6	4 5	sseqtrrid	Could not format ( ph -> S C_ ( F fldGen S ) ) : No typesetting found for |- ( ph -> S C_ ( F fldGen S ) ) with typecode |-