Theorem reldmmpl

Description: The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	reldmmpl	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPoly}$$

Proof

Step	Hyp	Ref	Expression
1		df-mpl	$$⊢\mathrm{mPoly}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼⦋\left(i\mathrm{mPwSer}r\right)/s⦌\left(s{\upharpoonright }_{𝑠}\left\{f\in {\mathrm{Base}}_s|{finSupp}_{0_r}\left(f\right)\right\}\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPoly}$$