clintopval

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

		Ref	Expression
	Assertion	clintopval	$⊢ M \in V \to clIntOp (M) = M^{(M \times M)}$

Step	Hyp	Ref	Expression
1		df-clintop	$⊢ clIntOp = (m \in V ⟼ m intOp m)$
2		id	$⊢ m = M \to m = M$
3	2 2	oveq12d	$⊢ m = M \to m intOp m = M intOp M$
4		intopval	$⊢ (M \in V \land M \in V) \to M intOp M = M^{(M \times M)}$
5	4	anidms	$⊢ M \in V \to M intOp M = M^{(M \times M)}$
6	3 5	sylan9eqr	$⊢ (M \in V \land m = M) \to m intOp m = M^{(M \times M)}$
7		elex	$⊢ M \in V \to M \in V$
8		ovexd	$⊢ M \in V \to M^{(M \times M)} \in V$
9	1 6 7 8	fvmptd2	$⊢ M \in V \to clIntOp (M) = M^{(M \times M)}$

Metamath Proof Explorer