Definition df-intop 45345

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 45342	. 2 class intOp
2		vm	. . 3 setvar 𝑚
3		vn	. . 3 setvar 𝑛
4		cvv 3430	. . 3 class V
5	3	cv 1540	. . . 4 class 𝑛
6	2	cv 1540	. . . . 5 class 𝑚
7	6, 6	cxp 5586	. . . 4 class (𝑚 × 𝑚)
8		cmap 8589	. . . 4 class ↑m
9	5, 7, 8	co 7268	. . 3 class (𝑛 ↑m (𝑚 × 𝑚))
10	2, 3, 4, 4, 9	cmpo 7270	. 2 class (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑m (𝑚 × 𝑚)))
11	1, 10	wceq 1541	1 wff intOp = (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑m (𝑚 × 𝑚)))

This definition is referenced by:  intopval  45348  intop  45349