Theorem reldmdsmm

Description: The direct sum is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015)

	Ref	Expression
Assertion	reldmdsmm	$$⊢\mathrm{Rel}\mathrm{dom}{\oplus }_m$$

Proof

Step	Hyp	Ref	Expression
1		df-dsmm	$$⊢{\oplus }_m=\left(s\in \mathrm{V},r\in \mathrm{V}⟼\left(s{⨉}_{𝑠}r\right){\upharpoonright }_{𝑠}\left\{f\in \underset{x\in \mathrm{dom}r}{⨉}{\mathrm{Base}}_{r\left(x\right)}|\left\{x\in \mathrm{dom}r|f\left(x\right)\ne 0_{r\left(x\right)}\right\}\in \mathrm{Fin}\right\}\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\oplus }_m$$