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 = ( 𝑚 ∈ V , 𝑛 ∈ V ↦ ( 𝑛 ↑m ( 𝑚 × 𝑚 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cintop	⊢ intOp
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		vn	⊢ 𝑛
4	3	cv	⊢ 𝑛
5		cmap	⊢ ↑m
6	1	cv	⊢ 𝑚
7	6 6	cxp	⊢ ( 𝑚 × 𝑚 )
8	4 7 5	co	⊢ ( 𝑛 ↑m ( 𝑚 × 𝑚 ) )
9	1 3 2 2 8	cmpo	⊢ ( 𝑚 ∈ V , 𝑛 ∈ V ↦ ( 𝑛 ↑m ( 𝑚 × 𝑚 ) ) )
10	0 9	wceq	⊢ intOp = ( 𝑚 ∈ V , 𝑛 ∈ V ↦ ( 𝑛 ↑m ( 𝑚 × 𝑚 ) ) )