Definition df-intop 48061

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 48058	. 2 class intOp
2		vm	. . 3 setvar 𝑚
3		vn	. . 3 setvar 𝑛
4		cvv 3464	. . 3 class V
5	3	cv 1538	. . . 4 class 𝑛
6	2	cv 1538	. . . . 5 class 𝑚
7	6, 6	cxp 5665	. . . 4 class (𝑚 × 𝑚)
8		cmap 8849	. . . 4 class ↑m
9	5, 7, 8	co 7414	. . 3 class (𝑛 ↑m (𝑚 × 𝑚))
10	2, 3, 4, 4, 9	cmpo 7416	. 2 class (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑m (𝑚 × 𝑚)))
11	1, 10	wceq 1539	1 wff intOp = (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑m (𝑚 × 𝑚)))

This definition is referenced by:  intopval  48064  intop  48065