Theorem reldmevls1

Description: Well-behaved binary operation property of evalSub1 . (Contributed by AV, 7-Sep-2019)

	Ref	Expression
Assertion	reldmevls1	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{evalSub}}_1$$

Proof

Step	Hyp	Ref	Expression
1		df-evls1	$$⊢{\mathrm{evalSub}}_1=\left(s\in \mathrm{V},r\in 𝒫{\mathrm{Base}}_s⟼⦋{\mathrm{Base}}_s/b⦌\left(\left(x\in \left(b^{\left(b^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in b⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{evalSub}s\right)\left(r\right)\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{evalSub}}_1$$