intopval

Description: The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020)

		Ref	Expression
	Assertion	intopval	$⊢ (M \in V \land N \in W) \to M intOp N = N^{(M \times M)}$

Step	Hyp	Ref	Expression
1		df-intop	$⊢ intOp = (m \in V, n \in V ⟼ n^{(m \times m)})$
2	1	a1i	$⊢ (M \in V \land N \in W) \to intOp = (m \in V, n \in V ⟼ n^{(m \times m)})$
3		simpr	$⊢ (m = M \land n = N) \to n = N$
4		simpl	$⊢ (m = M \land n = N) \to m = M$
5	4	sqxpeqd	$⊢ (m = M \land n = N) \to m \times m = M \times M$
6	3 5	oveq12d	$⊢ (m = M \land n = N) \to n^{(m \times m)} = N^{(M \times M)}$
7	6	adantl	$⊢ ((M \in V \land N \in W) \land (m = M \land n = N)) \to n^{(m \times m)} = N^{(M \times M)}$
8		elex	$⊢ M \in V \to M \in V$
9	8	adantr	$⊢ (M \in V \land N \in W) \to M \in V$
10		elex	$⊢ N \in W \to N \in V$
11	10	adantl	$⊢ (M \in V \land N \in W) \to N \in V$
12		ovexd	$⊢ (M \in V \land N \in W) \to N^{(M \times M)} \in V$
13	2 7 9 11 12	ovmpod	$⊢ (M \in V \land N \in W) \to M intOp N = N^{(M \times M)}$

Metamath Proof Explorer