Theorem reldmmpl

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

	Ref	Expression
Assertion	reldmmpl	⊢ Rel dom mPoly

Proof

Step	Hyp	Ref	Expression
1		df-mpl	⊢ mPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ⦋ ( 𝑖 mPwSer 𝑟 ) / 𝑠 ⦌ ( 𝑠 ↾s { 𝑓 ∈ ( Base ‘ 𝑠 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } ) )
2	1	reldmmpo	⊢ Rel dom mPoly