Theorem reldmpsr

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

	Ref	Expression
Assertion	reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$

Proof

Step	Hyp	Ref	Expression
1		df-psr	$$⊢\mathrm{mPwSer}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼⦋\left\{h\in \left({{\mathbb{N}}_0}^i\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}/d⦌⦋\left({{\mathrm{Base}}_r}^d\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_r\upharpoonright }_{\left(b\times b\right)}⟩,⟨{\cdot }_{\mathrm{ndx}},\left(f\in b,g\in b⟼\left(k\in d⟼\underset{x\in \left\{y\in d|y{\le }_{f}k\right\}}{{\sum }_r}\left(f\left(x\right){\cdot }_{r}g\left(k{-}_{f}x\right)\right)\right)\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),r⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_r,f\in b⟼\left(d\times \left\{x\right\}\right){{\cdot }_r}_{f}f\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(d\times \left\{\mathrm{TopOpen}\left(r\right)\right\}\right)⟩\right\}\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$