Definition df-intop 44105

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

Assertion

Ref	Expression
df-intop	⊢ intOp = (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑m (𝑚 × 𝑚)))

Distinct variable group:   𝑚,𝑛

Detailed syntax breakdown of Definition df-intop

Step	Hyp	Ref	Expression
1		cintop 44102	. 2 class intOp
2		vm	. . 3 setvar 𝑚
3		vn	. . 3 setvar 𝑛
4		cvv 3494	. . 3 class V
5	3	cv 1532	. . . 4 class 𝑛
6	2	cv 1532	. . . . 5 class 𝑚
7	6, 6	cxp 5552	. . . 4 class (𝑚 × 𝑚)
8		cmap 8405	. . . 4 class ↑m
9	5, 7, 8	co 7155	. . 3 class (𝑛 ↑m (𝑚 × 𝑚))
10	2, 3, 4, 4, 9	cmpo 7157	. 2 class (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑m (𝑚 × 𝑚)))
11	1, 10	wceq 1533	1 wff intOp = (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑m (𝑚 × 𝑚)))

This definition is referenced by:  intopval  44108  intop  44109