Metamath Proof Explorer


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 𝑀 } )