Metamath Proof Explorer

Definition df-intop

Description: Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020)

Ref Expression
Assertion df-intop 
|- intOp = ( m e. _V , n e. _V |-> ( n ^m ( m X. m ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cintop 
 |-  intOp
1 vm 
 |-  m
2 cvv 
 |-  _V
3 vn 
 |-  n
4 3 cv 
 |-  n
5 cmap 
 |-  ^m
6 1 cv 
 |-  m
7 6 6 cxp 
 |-  ( m X. m )
8 4 7 5 co 
 |-  ( n ^m ( m X. m ) )
9 1 3 2 2 8 cmpo 
 |-  ( m e. _V , n e. _V |-> ( n ^m ( m X. m ) ) )
10 0 9 wceq 
 |-  intOp = ( m e. _V , n e. _V |-> ( n ^m ( m X. m ) ) )