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