Metamath Proof Explorer


Theorem isclintop

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 ‘ 𝑀 ) ↔ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) )

Proof

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 ‘ 𝑀 ) ↔ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) )