Metamath Proof Explorer

Theorem clintopval

Description: The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020)

Ref Expression
Assertion clintopval 
|- ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) )

Proof

Step Hyp Ref Expression
1 df-clintop 
 |-  clIntOp = ( m e. _V |-> ( m intOp m ) )
2 id 
 |-  ( m = M -> m = M )
3 2 2 oveq12d 
 |-  ( m = M -> ( m intOp m ) = ( M intOp M ) )
4 intopval 
 |-  ( ( M e. V /\ M e. V ) -> ( M intOp M ) = ( M ^m ( M X. M ) ) )
5 4 anidms 
 |-  ( M e. V -> ( M intOp M ) = ( M ^m ( M X. M ) ) )
6 3 5 sylan9eqr 
 |-  ( ( M e. V /\ m = M ) -> ( m intOp m ) = ( M ^m ( M X. M ) ) )
7 elex 
 |-  ( M e. V -> M e. _V )
8 ovexd 
 |-  ( M e. V -> ( M ^m ( M X. M ) ) e. _V )
9 1 6 7 8 fvmptd2 
 |-  ( M e. V -> ( clIntOp ` M ) = ( M ^m ( M X. M ) ) )