Theorem assintopmap

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

	Ref	Expression
Assertion	assintopmap	⊢ ( 𝑀 ∈ 𝑉 → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } )

Proof

Step	Hyp	Ref	Expression
1		assintopval	⊢ ( 𝑀 ∈ 𝑉 → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } )
2		clintopval	⊢ ( 𝑀 ∈ 𝑉 → ( clIntOp ‘ 𝑀 ) = ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) )
3	2	rabeqdv	⊢ ( 𝑀 ∈ 𝑉 → { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } = { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } )
4	1 3	eqtrd	⊢ ( 𝑀 ∈ 𝑉 → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } )