Theorem clintopval

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

	Ref	Expression
Assertion	clintopval	⊢ ( 𝑀 ∈ 𝑉 → ( clIntOp ‘ 𝑀 ) = ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-clintop	⊢ clIntOp = ( 𝑚 ∈ V ↦ ( 𝑚 intOp 𝑚 ) )
2		id	⊢ ( 𝑚 = 𝑀 → 𝑚 = 𝑀 )
3	2 2	oveq12d	⊢ ( 𝑚 = 𝑀 → ( 𝑚 intOp 𝑚 ) = ( 𝑀 intOp 𝑀 ) )
4		intopval	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ) → ( 𝑀 intOp 𝑀 ) = ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) )
5	4	anidms	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 intOp 𝑀 ) = ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) )
6	3 5	sylan9eqr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑚 = 𝑀 ) → ( 𝑚 intOp 𝑚 ) = ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) )
7		elex	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
8		ovexd	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∈ V )
9	1 6 7 8	fvmptd2	⊢ ( 𝑀 ∈ 𝑉 → ( clIntOp ‘ 𝑀 ) = ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) )