Definition df-fldgen

Description: Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg ). If the base structure is a field, this is a subfield (see fldgenfld and fldsdrgfld ). In general this will be used in the context of fields, hence the name fldGen . (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025)

	Ref	Expression
Assertion	df-fldgen	$$⊢\mathrm{fldGen}=\left(f\in \mathrm{V},s\in \mathrm{V}⟼\bigcap \left\{a\in \mathrm{SubDRing}\left(f\right)|s\subseteq a\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfldgen	$$class\mathrm{fldGen}$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		va	$$setvara$$
5		csdrg	$$class\mathrm{SubDRing}$$
6	1	cv	$$setvarf$$
7	6 5	cfv	$$class\mathrm{SubDRing}\left(f\right)$$
8	3	cv	$$setvars$$
9	4	cv	$$setvara$$
10	8 9	wss	$$wffs\subseteq a$$
11	10 4 7	crab	$$class\left\{a\in \mathrm{SubDRing}\left(f\right)|s\subseteq a\right\}$$
12	11	cint	$$class\bigcap \left\{a\in \mathrm{SubDRing}\left(f\right)|s\subseteq a\right\}$$
13	1 3 2 2 12	cmpo	$$class\left(f\in \mathrm{V},s\in \mathrm{V}⟼\bigcap \left\{a\in \mathrm{SubDRing}\left(f\right)|s\subseteq a\right\}\right)$$
14	0 13	wceq	$$wff\mathrm{fldGen}=\left(f\in \mathrm{V},s\in \mathrm{V}⟼\bigcap \left\{a\in \mathrm{SubDRing}\left(f\right)|s\subseteq a\right\}\right)$$