Definition df-frac

Description: Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025)

	Ref	Expression
Assertion	df-frac	$$⊢\mathrm{Frac}=\left(r\in \mathrm{V}⟼r\mathrm{RLocal}\mathrm{RLReg}\left(r\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrac	$$class\mathrm{Frac}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarr$$
4		crloc	$$class\mathrm{RLocal}$$
5		crlreg	$$class\mathrm{RLReg}$$
6	3 5	cfv	$$class\mathrm{RLReg}\left(r\right)$$
7	3 6 4	co	$$class\left(r\mathrm{RLocal}\mathrm{RLReg}\left(r\right)\right)$$
8	1 2 7	cmpt	$$class\left(r\in \mathrm{V}⟼r\mathrm{RLocal}\mathrm{RLReg}\left(r\right)\right)$$
9	0 8	wceq	$$wff\mathrm{Frac}=\left(r\in \mathrm{V}⟼r\mathrm{RLocal}\mathrm{RLReg}\left(r\right)\right)$$