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	⊢ fldGen = ( 𝑓 ∈ V , 𝑠 ∈ V ↦ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfldgen	⊢ fldGen
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		va	⊢ 𝑎
5		csdrg	⊢ SubDRing
6	1	cv	⊢ 𝑓
7	6 5	cfv	⊢ ( SubDRing ‘ 𝑓 )
8	3	cv	⊢ 𝑠
9	4	cv	⊢ 𝑎
10	8 9	wss	⊢ 𝑠 ⊆ 𝑎
11	10 4 7	crab	⊢ { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 }
12	11	cint	⊢ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 }
13	1 3 2 2 12	cmpo	⊢ ( 𝑓 ∈ V , 𝑠 ∈ V ↦ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 } )
14	0 13	wceq	⊢ fldGen = ( 𝑓 ∈ V , 𝑠 ∈ V ↦ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 } )

Metamath Proof Explorer

Definition df-fldgen

Detailed syntax breakdown