Metamath Proof Explorer

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 = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / s ]_ ( s |`s { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } ) )
2 1 reldmmpo 
 |-  Rel dom mPoly