Definition df-fldgen 33919

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 33922). If the base structure is a field, this is a subfield (see fldgenfld 33928 and fldsdrgfld 21060). 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 33918	. 2 class fldGen
2		vf	. . 3 setvar 𝑓
3		vs	. . 3 setvar 𝑠
4		cvv 3450	. . 3 class V
5	3	cv 1568	. . . . . 6 class 𝑠
6		va	. . . . . . 7 setvar 𝑎
7	6	cv 1568	. . . . . 6 class 𝑎
8	5, 7	wss 3895	. . . . 5 wff 𝑠 ⊆ 𝑎
9	2	cv 1568	. . . . . 6 class 𝑓
10		csdrg 21048	. . . . . 6 class SubDRing
11	9, 10	cfv 6538	. . . . 5 class (SubDRing‘𝑓)
12	8, 6, 11	crab 3412	. . . 4 class {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎}
13	12	cint 4906	. . 3 class ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎}
14	2, 3, 4, 4, 13	cmpo 7422	. 2 class (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎})
15	1, 14	wceq 1569	1 wff fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎})

This definition is used by:  fldgenval  33920