Definition df-fldgen 32904

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 32907). If the base structure is a field, this is a subfield (see fldgenfld 32913 and fldsdrgfld 20649). 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.)

Assertion

Ref	Expression
df-fldgen	⊢ fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎})

Distinct variable group:   𝑓,𝑠,𝑎

Detailed syntax breakdown of Definition df-fldgen

Step	Hyp	Ref	Expression
1		cfldgen 32903	. 2 class fldGen
2		vf	. . 3 setvar 𝑓
3		vs	. . 3 setvar 𝑠
4		cvv 3468	. . 3 class V
5	3	cv 1532	. . . . . 6 class 𝑠
6		va	. . . . . . 7 setvar 𝑎
7	6	cv 1532	. . . . . 6 class 𝑎
8	5, 7	wss 3943	. . . . 5 wff 𝑠 ⊆ 𝑎
9	2	cv 1532	. . . . . 6 class 𝑓
10		csdrg 20637	. . . . . 6 class SubDRing
11	9, 10	cfv 6537	. . . . 5 class (SubDRing‘𝑓)
12	8, 6, 11	crab 3426	. . . 4 class {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎}
13	12	cint 4943	. . 3 class ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎}
14	2, 3, 4, 4, 13	cmpo 7407	. 2 class (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎})
15	1, 14	wceq 1533	1 wff fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎})

This definition is referenced by:  fldgenval  32905