Definition df-intop 41625

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 ↦ (𝑛 ↑𝑚 (𝑚 × 𝑚)))

Distinct variable group:   𝑚,𝑛

Detailed syntax breakdown of Definition df-intop

Step	Hyp	Ref	Expression
1		cintop 41622	. 2 class intOp
2		vm	. . 3 setvar 𝑚
3		vn	. . 3 setvar 𝑛
4		cvv 3173	. . 3 class V
5	3	cv 1474	. . . 4 class 𝑛
6	2	cv 1474	. . . . 5 class 𝑚
7	6, 6	cxp 5036	. . . 4 class (𝑚 × 𝑚)
8		cmap 7744	. . . 4 class ↑𝑚
9	5, 7, 8	co 6549	. . 3 class (𝑛 ↑𝑚 (𝑚 × 𝑚))
10	2, 3, 4, 4, 9	cmpt2 6551	. 2 class (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑𝑚 (𝑚 × 𝑚)))
11	1, 10	wceq 1475	1 wff intOp = (𝑚 ∈ V, 𝑛 ∈ V ↦ (𝑛 ↑𝑚 (𝑚 × 𝑚)))

This definition is referenced by:  intopval  41628  intop  41629