Description: The predicate "is a closed (internal binary) operations for a set". (Contributed by FL, 2-Nov-2009) (Revised by AV, 20-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | isclintop | ⊢ ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ↔ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clintopval | ⊢ ( 𝑀 ∈ 𝑉 → ( clIntOp ‘ 𝑀 ) = ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ) | |
2 | 1 | eleq2d | ⊢ ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ↔ ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ) ) |
3 | sqxpexg | ⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 × 𝑀 ) ∈ V ) | |
4 | elmapg | ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝑀 × 𝑀 ) ∈ V ) → ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ↔ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) ) | |
5 | 3 4 | mpdan | ⊢ ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ↔ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) ) |
6 | 2 5 | bitrd | ⊢ ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ↔ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) ) |