Metamath Proof Explorer

Theorem intopval

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

Ref Expression
Assertion intopval 
|- ( ( M e. V /\ N e. W ) -> ( M intOp N ) = ( N ^m ( M X. M ) ) )

Proof

Step Hyp Ref Expression
1 df-intop 
 |-  intOp = ( m e. _V , n e. _V |-> ( n ^m ( m X. m ) ) )
2 1 a1i 
 |-  ( ( M e. V /\ N e. W ) -> intOp = ( m e. _V , n e. _V |-> ( n ^m ( m X. m ) ) ) )
3 simpr 
 |-  ( ( m = M /\ n = N ) -> n = N )
4 simpl 
 |-  ( ( m = M /\ n = N ) -> m = M )
5 4 sqxpeqd 
 |-  ( ( m = M /\ n = N ) -> ( m X. m ) = ( M X. M ) )
6 3 5 oveq12d 
 |-  ( ( m = M /\ n = N ) -> ( n ^m ( m X. m ) ) = ( N ^m ( M X. M ) ) )
7 6 adantl 
 |-  ( ( ( M e. V /\ N e. W ) /\ ( m = M /\ n = N ) ) -> ( n ^m ( m X. m ) ) = ( N ^m ( M X. M ) ) )
8 elex 
 |-  ( M e. V -> M e. _V )
9 8 adantr 
 |-  ( ( M e. V /\ N e. W ) -> M e. _V )
10 elex 
 |-  ( N e. W -> N e. _V )
11 10 adantl 
 |-  ( ( M e. V /\ N e. W ) -> N e. _V )
12 ovexd 
 |-  ( ( M e. V /\ N e. W ) -> ( N ^m ( M X. M ) ) e. _V )
13 2 7 9 11 12 ovmpod 
 |-  ( ( M e. V /\ N e. W ) -> ( M intOp N ) = ( N ^m ( M X. M ) ) )